\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{TOP002-2.p} Topology generated by a basis forms a topological space, part 2






$\mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ or }\mbox{element\_of\_set}(f_{11}(\mbox{vf},u),u)\qquad\mbox{cnf}(\mbox{topology\_generated}_{40},\mbox{axiom})$

$\neg\,\mbox{element\_of\_set}(x,\mbox{empty\_set})\qquad\mbox{cnf}(\mbox{set\_theory}_6,\mbox{axiom})$

$\neg\,\mbox{element\_of\_collection}(\mbox{empty\_set},\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1b}_2,\mbox{negated\_conjecture})$

\medskip\textbf{TOP017-1.p} If the boundary of A is empty, A is both open and closed






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{topological\_space}(\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_12}_{154},\mbox{negated\_conjecture})$

$\mbox{subset\_sets}(a,\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_12}_{155},\mbox{negated\_conjecture})$

$\mbox{equal\_sets}(\mbox{boundary}(a,\mbox{cx},\mbox{ct}),\mbox{empty\_set})\mbox{ or }\mbox{open}(a,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_12}_{156},\mbox{negated\_conjecture})$

$\mbox{equal\_sets}(\mbox{boundary}(a,\mbox{cx},\mbox{ct}),\mbox{empty\_set})\mbox{ or }\mbox{closed}(a,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_12}_{157},\mbox{negated\_conjecture})$

$( \mbox{equal\_sets}(\mbox{boundary}(a,\mbox{cx},\mbox{ct}),\mbox{empty\_set})\mbox{ and }\mbox{open}(a,\mbox{cx},\mbox{ct}) ) \ \Rightarrow \ \neg\,\mbox{closed}(a,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_12}_{158},\mbox{negated\_conjecture})$

\medskip\textbf{TOP008-1.p} The subspace topology gives rise to a topological space






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{topological\_space}(\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_3}_{117},\mbox{negated\_conjecture})$

$\mbox{subset\_sets}(\mbox{cy},\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_3}_{118},\mbox{negated\_conjecture})$

$\neg\,\mbox{topological\_space}(\mbox{cy},\mbox{subspace\_topology}(\mbox{cx},\mbox{ct},\mbox{cy}))\qquad\mbox{cnf}(\mbox{problem\_3}_{119},\mbox{negated\_conjecture})$

\medskip\textbf{TOP001-2.p} Topology generated by a basis forms a topological space, part 1






$\mbox{element\_of\_set}(u,\mbox{union\_of\_members}(\mbox{vf})) \ \Rightarrow \ \mbox{element\_of\_set}(u,f_1(\mbox{vf},u))\qquad\mbox{cnf}(\mbox{union\_of\_members}_1,\mbox{axiom})$

$\mbox{element\_of\_set}(u,\mbox{union\_of\_members}(\mbox{vf})) \ \Rightarrow \ \mbox{element\_of\_collection}(f_1(\mbox{vf},u),\mbox{vf})\qquad\mbox{cnf}(\mbox{union\_of\_members}_2,\mbox{axiom})$

$( \mbox{element\_of\_set}(u,\mbox{uu}_1)\mbox{ and }\mbox{element\_of\_collection}(\mbox{uu}_1,\mbox{vf}) ) \ \Rightarrow \ \mbox{element\_of\_set}(u,\mbox{union\_of\_members}(\mbox{vf}))\qquad\mbox{cnf}(\mbox{union\_of\_members}_3,\mbox{axiom})$

$\mbox{basis}(x,\mbox{vf}) \ \Rightarrow \ \mbox{equal\_sets}(\mbox{union\_of\_members}(\mbox{vf}),x)\qquad\mbox{cnf}(\mbox{basis\_for\_topology}_{28},\mbox{axiom})$

$( \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ and }\mbox{element\_of\_set}(x,u) ) \ \Rightarrow \ \mbox{element\_of\_set}(x,f_{10}(\mbox{vf},u,x))\qquad\mbox{cnf}(\mbox{topology\_generated}_{37},\mbox{axiom})$

$( \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ and }\mbox{element\_of\_set}(x,u) ) \ \Rightarrow \ \mbox{element\_of\_collection}(f_{10}(\mbox{vf},u,x),\mbox{vf})\qquad\mbox{cnf}(\mbox{topology\_generated}_{38},\mbox{axiom})$

$\mbox{subset\_sets}(x,x)\qquad\mbox{cnf}(\mbox{set\_theory}_1,\mbox{axiom})$

$( \mbox{subset\_sets}(x,y)\mbox{ and }\mbox{element\_of\_set}(u,x) ) \ \Rightarrow \ \mbox{element\_of\_set}(u,y)\qquad\mbox{cnf}(\mbox{set\_theory}_2,\mbox{axiom})$

$\mbox{equal\_sets}(x,y) \ \Rightarrow \ \mbox{subset\_sets}(x,y)\qquad\mbox{cnf}(\mbox{set\_theory}_3,\mbox{axiom})$

$\mbox{subset\_sets}(x,y)\mbox{ or }\mbox{element\_of\_set}(\mbox{in\_1st\_set}(x,y),x)\qquad\mbox{cnf}(\mbox{set\_theory}_4,\mbox{axiom})$

$\mbox{element\_of\_set}(\mbox{in\_1st\_set}(x,y),y) \ \Rightarrow \ \mbox{subset\_sets}(x,y)\qquad\mbox{cnf}(\mbox{set\_theory}_5,\mbox{axiom})$

$\mbox{basis}(\mbox{cx},f)\qquad\mbox{cnf}(\mbox{lemma\_1a}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{subset\_sets}(\mbox{union\_of\_members}(\mbox{top\_of\_basis}(f)),\mbox{cx})\qquad\mbox{cnf}(\mbox{lemma\_1a}_2,\mbox{negated\_conjecture})$

\medskip\textbf{TOP006-1.p} Topology generated by a basis forms a topological space






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{basis}(\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_1}_{110},\mbox{negated\_conjecture})$

$\neg\,\mbox{topological\_space}(\mbox{cx},\mbox{top\_of\_basis}(\mbox{ct}))\qquad\mbox{cnf}(\mbox{problem\_1}_{111},\mbox{negated\_conjecture})$

\medskip\textbf{TOP009-1.p} If Y is open in X, and A is open in Y, then A is open in X






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{open}(\mbox{cy},\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_4}_{120},\mbox{negated\_conjecture})$

$\mbox{open}(a,\mbox{cy},\mbox{subspace\_topology}(\mbox{cx},\mbox{ct},\mbox{cy}))\qquad\mbox{cnf}(\mbox{problem\_4}_{121},\mbox{negated\_conjecture})$

$\neg\,\mbox{open}(a,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_4}_{122},\mbox{negated\_conjecture})$

\medskip\textbf{TOP007-1.p} Property 1 of topological spaces

If (cx,ct) is a topological space, A is a subset of X, and
 every point in A has a neighborhood U that is a subset of A,
 then A is open in (cx,ct).




$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{topological\_space}(\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_2}_{112},\mbox{negated\_conjecture})$

$\mbox{subset\_sets}(a,\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_2}_{113},\mbox{negated\_conjecture})$

$\mbox{element\_of\_set}(y,a) \ \Rightarrow \ \mbox{neighborhood}(f_{30}(y),y,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_2}_{114},\mbox{negated\_conjecture})$

$\mbox{element\_of\_set}(y,a) \ \Rightarrow \ \mbox{subset\_sets}(f_{30}(y),a)\qquad\mbox{cnf}(\mbox{problem\_2}_{115},\mbox{negated\_conjecture})$

$\neg\,\mbox{open}(a,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_2}_{116},\mbox{negated\_conjecture})$

\medskip\textbf{TOP015-1.p} The interior and the boundary of a set are disjoint






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{topological\_space}(\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_10}_{148},\mbox{negated\_conjecture})$

$\mbox{subset\_sets}(a,\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_10}_{149},\mbox{negated\_conjecture})$

$\neg\,\mbox{equal\_sets}(\mbox{intersection\_of\_sets}(\mbox{interior}(a,\mbox{cx},\mbox{ct}),\mbox{boundary}(a,\mbox{cx},\mbox{ct})),\mbox{empty\_set})\qquad\mbox{cnf}(\mbox{problem\_10}_{150},\mbox{negated\_conjecture})$

\medskip\textbf{TOP018-1.p} Propoerty of limits points and connected sets

If limit points are added to a connected set, the result is
 connected.




$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{connected\_set}(a,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_13}_{159},\mbox{negated\_conjecture})$

$\mbox{element\_of\_set}(y,b) \ \Rightarrow \ \mbox{limit\_point}(y,a,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_13}_{160},\mbox{negated\_conjecture})$

$\neg\,\mbox{connected\_set}(\mbox{union\_of\_sets}(a,b),\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_13}_{161},\mbox{negated\_conjecture})$

\medskip\textbf{TOP013-1.p} Properties of interior and closure

The interior of A is a subset of A, which is a subset of the
 closure of A.




$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{topological\_space}(\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_8}_{139},\mbox{negated\_conjecture})$

$\mbox{subset\_sets}(a,\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_8}_{140},\mbox{negated\_conjecture})$

$\mbox{subset\_sets}(\mbox{interior}(a,\mbox{cx},\mbox{ct}),a) \ \Rightarrow \ \neg\,\mbox{subset\_sets}(a,\mbox{closure}(a,\mbox{cx},\mbox{ct}))\qquad\mbox{cnf}(\mbox{problem\_8}_{141},\mbox{negated\_conjecture})$

\medskip\textbf{TOP001-1.p} Topology generated by a basis forms a topological space, part 1






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{basis}(\mbox{cx},f)\qquad\mbox{cnf}(\mbox{lemma\_1a}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{subset\_sets}(\mbox{union\_of\_members}(\mbox{top\_of\_basis}(f)),\mbox{cx})\qquad\mbox{cnf}(\mbox{lemma\_1a}_2,\mbox{negated\_conjecture})$

\medskip\textbf{TOP011-1.p} An alternative definition of top\_of\_basis






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{element\_of\_set}(\mbox{cu},\mbox{top\_of\_basis}(f))\mbox{ or }\mbox{subset\_collections}(g,f)\qquad\mbox{cnf}(\mbox{problem\_6}_{126},\mbox{negated\_conjecture})$

$\mbox{element\_of\_set}(\mbox{cu},\mbox{top\_of\_basis}(f))\mbox{ or }\mbox{equal\_sets}(\mbox{cu},\mbox{union\_of\_members}(g))\qquad\mbox{cnf}(\mbox{problem\_6}_{127},\mbox{negated\_conjecture})$

$( \mbox{element\_of\_set}(\mbox{cu},\mbox{top\_of\_basis}(f))\mbox{ and }\mbox{subset\_collections}(x,f) ) \ \Rightarrow \ \neg\,\mbox{equal\_sets}(\mbox{cu},\mbox{union\_of\_members}(x))\qquad\mbox{cnf}(\mbox{problem\_6}_{128},\mbox{negated\_conjecture})$

\medskip\textbf{TOP016-1.p} The union of the interior and the boundary is the closure






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{topological\_space}(\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_11}_{151},\mbox{negated\_conjecture})$

$\mbox{subset\_sets}(a,\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_11}_{152},\mbox{negated\_conjecture})$

$\neg\,\mbox{equal\_sets}(\mbox{union\_of\_sets}(\mbox{interior}(a,\mbox{cx},\mbox{ct}),\mbox{boundary}(a,\mbox{cx},\mbox{ct})),\mbox{closure}(a,\mbox{cx},\mbox{ct}))\qquad\mbox{cnf}(\mbox{problem\_11}_{153},\mbox{negated\_conjecture})$

\medskip\textbf{TOP003-2.p} Topology generated by a basis forms a topological space, part 3






$\mbox{element\_of\_set}(u,\mbox{union\_of\_members}(\mbox{vf})) \ \Rightarrow \ \mbox{element\_of\_set}(u,f_1(\mbox{vf},u))\qquad\mbox{cnf}(\mbox{union\_of\_members}_1,\mbox{axiom})$

$\mbox{element\_of\_set}(u,\mbox{union\_of\_members}(\mbox{vf})) \ \Rightarrow \ \mbox{element\_of\_collection}(f_1(\mbox{vf},u),\mbox{vf})\qquad\mbox{cnf}(\mbox{union\_of\_members}_2,\mbox{axiom})$

$\mbox{basis}(x,\mbox{vf}) \ \Rightarrow \ \mbox{equal\_sets}(\mbox{union\_of\_members}(\mbox{vf}),x)\qquad\mbox{cnf}(\mbox{basis\_for\_topology}_{28},\mbox{axiom})$

$\mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ or }\mbox{element\_of\_set}(f_{11}(\mbox{vf},u),u)\qquad\mbox{cnf}(\mbox{topology\_generated}_{40},\mbox{axiom})$

$\mbox{element\_of\_collection}(x,y) \ \Rightarrow \ \mbox{subset\_sets}(x,\mbox{union\_of\_members}(y))\qquad\mbox{cnf}(\mbox{set\_theory}_7,\mbox{axiom})$

$( \mbox{subset\_sets}(x,y)\mbox{ and }\mbox{element\_of\_set}(u,x) ) \ \Rightarrow \ \mbox{element\_of\_set}(u,y)\qquad\mbox{cnf}(\mbox{set\_theory}_8,\mbox{axiom})$

$\mbox{subset\_sets}(x,x)\qquad\mbox{cnf}(\mbox{set\_theory}_9,\mbox{axiom})$

$( \mbox{equal\_sets}(x,y)\mbox{ and }\mbox{subset\_sets}(z,x) ) \ \Rightarrow \ \mbox{subset\_sets}(z,y)\qquad\mbox{cnf}(\mbox{set\_theory}_{10},\mbox{axiom})$

$( \mbox{equal\_sets}(x,y)\mbox{ and }\mbox{subset\_sets}(x,z) ) \ \Rightarrow \ \mbox{subset\_sets}(y,z)\qquad\mbox{cnf}(\mbox{set\_theory}_{11},\mbox{axiom})$

$\mbox{basis}(\mbox{cx},f)\qquad\mbox{cnf}(\mbox{lemma\_1c}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{element\_of\_collection}(\mbox{cx},\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1c}_2,\mbox{negated\_conjecture})$

\medskip\textbf{TOP021+1.p} Locally compact tological space






$\forall a,x,a_1{:}\;\mbox{a\_continuous\_function\_from\_onto}(\mbox{the\_projection\_function}(a,x,a_1),\mbox{the\_product\_top\_space\_over}(x,a_1),\mbox{apply}(x,a))\qquad\mbox{fof}(\mbox{kelley\_p90a},\mbox{axiom})$

$\forall a,x,a_1,x_1{:}\;\mbox{an\_open\_function\_from\_onto}(\mbox{the\_projection\_function}(a,x,a_1),\mbox{the\_product\_top\_space\_over}(x_1,a_1),\mbox{apply}(x_1,a))\qquad\mbox{fof}(\mbox{kelley\_3}_2,\mbox{axiom})$

$\forall f,a,b{:}\;( ( \mbox{an\_open\_function\_from\_onto}(f,a,b)\mbox{ and }\mbox{a\_continuous\_function\_from\_onto}(f,a,b)\mbox{ and }\mbox{a\_locally\_compact\_top\_space}(a) ) \ \Rightarrow \ \mbox{a\_locally\_compact\_top\_space}(b) )\qquad\mbox{fof}(\mbox{kelley\_p\_147e},\mbox{axiom})$

$\forall x_1,a_1{:}\;( \mbox{a\_locally\_compact\_top\_space}(\mbox{the\_product\_top\_space\_over}(x_1,a_1)) \ \Rightarrow \ \forall a{:}\;\mbox{a\_locally\_compact\_top\_space}(\mbox{apply}(x_1,a)) )\qquad\mbox{fof}(\mbox{kelley\_5\_19a},\mbox{conjecture})$

\medskip\textbf{TOP004-1.p} Topology generated by a basis forms a topological space, part 4






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{basis}(\mbox{cx},f)\qquad\mbox{cnf}(\mbox{lemma\_1d}_1,\mbox{negated\_conjecture})$

$\mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1d}_2,\mbox{negated\_conjecture})$

$\mbox{element\_of\_collection}(v,\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1d}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{element\_of\_collection}(\mbox{intersection\_of\_sets}(u,v),\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1d}_4,\mbox{negated\_conjecture})$

\medskip\textbf{TOP004-2.p} Topology generated by a basis forms a topological space, part 4






$( \mbox{element\_of\_set}(u,\mbox{uu}_1)\mbox{ and }\mbox{element\_of\_collection}(\mbox{uu}_1,\mbox{vf}) ) \ \Rightarrow \ \mbox{element\_of\_set}(u,\mbox{union\_of\_members}(\mbox{vf}))\qquad\mbox{cnf}(\mbox{union\_of\_members}_3,\mbox{axiom})$

$\mbox{basis}(x,\mbox{vf}) \ \Rightarrow \ \mbox{equal\_sets}(\mbox{union\_of\_members}(\mbox{vf}),x)\qquad\mbox{cnf}(\mbox{basis\_for\_topology}_{28},\mbox{axiom})$

$( \mbox{basis}(x,\mbox{vf})\mbox{ and }\mbox{element\_of\_set}(y,x)\mbox{ and }\mbox{element\_of\_collection}(\mbox{vb}_1,\mbox{vf})\mbox{ and }\mbox{element\_of\_collection}(\mbox{vb}_2,\mbox{vf})\mbox{ and }\mbox{element\_of\_set}(y,\mbox{intersection\_of\_sets}(\mbox{vb}_1,\mbox{vb}_2)) ) \ \Rightarrow \ \mbox{element\_of\_set}(y,f_6(x,\mbox{vf},y,\mbox{vb}_1,\mbox{vb}_2))\qquad\mbox{cnf}(\mbox{basis\_for\_topology}_{29},\mbox{axiom})$

$( \mbox{basis}(x,\mbox{vf})\mbox{ and }\mbox{element\_of\_set}(y,x)\mbox{ and }\mbox{element\_of\_collection}(\mbox{vb}_1,\mbox{vf})\mbox{ and }\mbox{element\_of\_collection}(\mbox{vb}_2,\mbox{vf})\mbox{ and }\mbox{element\_of\_set}(y,\mbox{intersection\_of\_sets}(\mbox{vb}_1,\mbox{vb}_2)) ) \ \Rightarrow \ \mbox{element\_of\_collection}(f_6(x,\mbox{vf},y,\mbox{vb}_1,\mbox{vb}_2),\mbox{vf})\qquad\mbox{cnf}(\mbox{basis\_for\_topology}_{30},\mbox{axiom})$

$( \mbox{basis}(x,\mbox{vf})\mbox{ and }\mbox{element\_of\_set}(y,x)\mbox{ and }\mbox{element\_of\_collection}(\mbox{vb}_1,\mbox{vf})\mbox{ and }\mbox{element\_of\_collection}(\mbox{vb}_2,\mbox{vf})\mbox{ and }\mbox{element\_of\_set}(y,\mbox{intersection\_of\_sets}(\mbox{vb}_1,\mbox{vb}_2)) ) \ \Rightarrow \ \mbox{subset\_sets}(f_6(x,\mbox{vf},y,\mbox{vb}_1,\mbox{vb}_2),\mbox{intersection\_of\_sets}(\mbox{vb}_1,\mbox{vb}_2))\qquad\mbox{cnf}(\mbox{basis\_for\_topology}_{31},\mbox{axiom})$

$( \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ and }\mbox{element\_of\_set}(x,u) ) \ \Rightarrow \ \mbox{element\_of\_set}(x,f_{10}(\mbox{vf},u,x))\qquad\mbox{cnf}(\mbox{topology\_generated}_{37},\mbox{axiom})$

$( \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ and }\mbox{element\_of\_set}(x,u) ) \ \Rightarrow \ \mbox{element\_of\_collection}(f_{10}(\mbox{vf},u,x),\mbox{vf})\qquad\mbox{cnf}(\mbox{topology\_generated}_{38},\mbox{axiom})$

$( \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ and }\mbox{element\_of\_set}(x,u) ) \ \Rightarrow \ \mbox{subset\_sets}(f_{10}(\mbox{vf},u,x),u)\qquad\mbox{cnf}(\mbox{topology\_generated}_{39},\mbox{axiom})$

$\mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ or }\mbox{element\_of\_set}(f_{11}(\mbox{vf},u),u)\qquad\mbox{cnf}(\mbox{topology\_generated}_{40},\mbox{axiom})$

$( \mbox{element\_of\_set}(f_{11}(\mbox{vf},u),\mbox{uu}_{11})\mbox{ and }\mbox{element\_of\_collection}(\mbox{uu}_{11},\mbox{vf})\mbox{ and }\mbox{subset\_sets}(\mbox{uu}_{11},u) ) \ \Rightarrow \ \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\qquad\mbox{cnf}(\mbox{topology\_generated}_{41},\mbox{axiom})$

$( \mbox{subset\_sets}(x,y)\mbox{ and }\mbox{subset\_sets}(y,z) ) \ \Rightarrow \ \mbox{subset\_sets}(x,z)\qquad\mbox{cnf}(\mbox{set\_theory}_{12},\mbox{axiom})$

$\mbox{element\_of\_set}(z,\mbox{intersection\_of\_sets}(x,y)) \ \Rightarrow \ \mbox{element\_of\_set}(z,x)\qquad\mbox{cnf}(\mbox{set\_theory}_{13},\mbox{axiom})$

$\mbox{element\_of\_set}(z,\mbox{intersection\_of\_sets}(x,y)) \ \Rightarrow \ \mbox{element\_of\_set}(z,y)\qquad\mbox{cnf}(\mbox{set\_theory}_{14},\mbox{axiom})$

$( \mbox{element\_of\_set}(z,x)\mbox{ and }\mbox{element\_of\_set}(z,y) ) \ \Rightarrow \ \mbox{element\_of\_set}(z,\mbox{intersection\_of\_sets}(x,y))\qquad\mbox{cnf}(\mbox{set\_theory}_{15},\mbox{axiom})$

$( \mbox{subset\_sets}(x,y)\mbox{ and }\mbox{subset\_sets}(u,v) ) \ \Rightarrow \ \mbox{subset\_sets}(\mbox{intersection\_of\_sets}(x,u),\mbox{intersection\_of\_sets}(y,v))\qquad\mbox{cnf}(\mbox{set\_theory}_{16},\mbox{axiom})$

$( \mbox{equal\_sets}(x,y)\mbox{ and }\mbox{element\_of\_set}(z,x) ) \ \Rightarrow \ \mbox{element\_of\_set}(z,y)\qquad\mbox{cnf}(\mbox{set\_theory}_{17},\mbox{axiom})$

$\mbox{equal\_sets}(\mbox{intersection\_of\_sets}(x,y),\mbox{intersection\_of\_sets}(y,x))\qquad\mbox{cnf}(\mbox{set\_theory}_{18},\mbox{axiom})$

$\mbox{basis}(\mbox{cx},f)\qquad\mbox{cnf}(\mbox{lemma\_1d}_1,\mbox{negated\_conjecture})$

$\mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1d}_2,\mbox{negated\_conjecture})$

$\mbox{element\_of\_collection}(v,\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1d}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{element\_of\_collection}(\mbox{intersection\_of\_sets}(u,v),\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1d}_4,\mbox{negated\_conjecture})$

\medskip\textbf{TOP003-1.p} Topology generated by a basis forms a topological space, part 3






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{basis}(\mbox{cx},f)\qquad\mbox{cnf}(\mbox{lemma\_1c}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{element\_of\_collection}(\mbox{cx},\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1c}_2,\mbox{negated\_conjecture})$

\medskip\textbf{TOP020+1.p} Property of a Hausdorff topological space

In a Hausdorff topological space, the diagonal of the space
 is closed in the product of the space with itself.




$\forall x,a{:}\;( \forall y{:}\;( ( \mbox{a\_member\_of}(y,\mbox{coerce\_to\_class}(x))\mbox{ and }\neg\,\mbox{a\_member\_of}(y,a) ) \ \Rightarrow \ \exists g{:}\;( \mbox{a\_member\_of}(y,g)\mbox{ and }\mbox{open\_in}(g,x)\mbox{ and }\mbox{disjoint}(g,a) ) ) \ \Rightarrow \ \mbox{closed\_in}(a,x) )\qquad\mbox{fof}(\mbox{closed\_subset\_thm},\mbox{axiom})$

$\forall x{:}\;( \mbox{a\_hausdorff\_top\_space}(x) \ \Rightarrow \ \forall a,b{:}\;( ( \mbox{a\_member\_of}(a,\mbox{coerce\_to\_class}(x))\mbox{ and }\mbox{a\_member\_of}(b,\mbox{coerce\_to\_class}(x))\mbox{ and }a\ne b ) \ \Rightarrow \ \exists g_1,g_2{:}\;( \mbox{open\_in}(g_1,x)\mbox{ and }\mbox{open\_in}(g_2,x)\mbox{ and }\mbox{a\_member\_of}(a,g_1)\mbox{ and }\mbox{a\_member\_of}(b,g_2)\mbox{ and }\mbox{disjoint}(g_1,g_2) ) ) )\qquad\mbox{fof}(\mbox{hausdorff},\mbox{axiom})$

$\forall a,x,b,y{:}\;( ( \mbox{open\_in}(a,x)\mbox{ and }\mbox{open\_in}(b,y) ) \ \Rightarrow \ \mbox{open\_in}(\mbox{the\_product\_of}(a,b),\mbox{the\_product\_top\_space\_of}(x,y)) )\qquad\mbox{fof}(\mbox{product\_of\_open\_sets},\mbox{axiom})$

$\forall s,t,x{:}\;( \mbox{a\_member\_of}(x,\mbox{coerce\_to\_class}(\mbox{the\_product\_top\_space\_of}(s,t))) \ \Rightarrow \ \exists a,b{:}\;( \mbox{a\_member\_of}(a,\mbox{coerce\_to\_class}(s))\mbox{ and }\mbox{a\_member\_of}(b,\mbox{coerce\_to\_class}(t))\mbox{ and }x = \mbox{the\_ordered\_pair}(a,b) ) )\qquad\mbox{fof}(\mbox{product\_top},\mbox{axiom})$

$\forall x,s,t{:}\;( \mbox{a\_member\_of}(x,\mbox{the\_product\_of}(s,t))\iff \exists a,b{:}\;( \mbox{a\_member\_of}(a,s)\mbox{ and }\mbox{a\_member\_of}(b,t)\mbox{ and }x = \mbox{the\_ordered\_pair}(a,b) ) )\qquad\mbox{fof}(\mbox{product},\mbox{axiom})$

$\forall a,b{:}\;( \mbox{disjoint}(a,b)\iff \neg\,\exists y{:}\;( \mbox{a\_member\_of}(y,a)\mbox{ and }\mbox{a\_member\_of}(y,b) ) )\qquad\mbox{fof}(\mbox{disjoint\_defn},\mbox{axiom})$

$\forall a,b,c,d{:}\;( \mbox{the\_ordered\_pair}(a,b) = \mbox{the\_ordered\_pair}(c,d) \ \Rightarrow \ ( a = c\mbox{ and }b = d ) )\qquad\mbox{fof}(\mbox{ordered\_pair},\mbox{axiom})$

$\forall x,s{:}\;( \mbox{a\_member\_of}(x,\mbox{coerce\_to\_class}(\mbox{the\_diagonal\_top}(s)))\iff \exists a{:}\;( \mbox{a\_member\_of}(a,\mbox{coerce\_to\_class}(s))\mbox{ and }x = \mbox{the\_ordered\_pair}(a,a) ) )\qquad\mbox{fof}(\mbox{diagonal\_top},\mbox{axiom})$

$\forall s{:}\;( \mbox{a\_hausdorff\_top\_space}(s) \ \Rightarrow \ \mbox{closed\_in}(\mbox{coerce\_to\_class}(\mbox{the\_diagonal\_top}(s)),\mbox{the\_product\_top\_space\_of}(s,s)) )\qquad\mbox{fof}(\mbox{challenge\_AMR\_1\_4}_4,\mbox{conjecture})$

\medskip\textbf{TOP019-1.p} The closure of a connected set is connected






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{connected\_set}(a,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_14}_{162},\mbox{negated\_conjecture})$

$\neg\,\mbox{connected\_set}(\mbox{closure}(a,\mbox{cx},\mbox{ct}),\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_14}_{163},\mbox{negated\_conjecture})$

\medskip\textbf{TOP005-1.p} Topology generated by a basis forms a topological space, part 5






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{basis}(\mbox{cx},f)\qquad\mbox{cnf}(\mbox{lemma\_1e}_1,\mbox{negated\_conjecture})$

$\mbox{subset\_collections}(g,\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1e}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{element\_of\_collection}(\mbox{union\_of\_members}(g),\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1e}_3,\mbox{negated\_conjecture})$

\medskip\textbf{TOP014-1.p} Properties of open \& interior and closed \& closure

If A is open, the interior of A is A, and if A is closed, the
 closure of A is A.




$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{topological\_space}(\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_9}_{142},\mbox{negated\_conjecture})$

$\mbox{subset\_sets}(a,\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_9}_{143},\mbox{negated\_conjecture})$

$\mbox{open}(a,\mbox{cx},\mbox{ct})\mbox{ or }\mbox{equal\_sets}(a,\mbox{interior}(a,\mbox{cx},\mbox{ct}))\mbox{ or }\mbox{closed}(a,\mbox{cx},\mbox{ct})\mbox{ or }\mbox{equal\_sets}(a,\mbox{closure}(a,\mbox{cx},\mbox{ct}))\qquad\mbox{cnf}(\mbox{problem\_9}_{144},\mbox{negated\_conjecture})$

$( \mbox{closed}(a,\mbox{cx},\mbox{ct})\mbox{ and }\mbox{equal\_sets}(a,\mbox{closure}(a,\mbox{cx},\mbox{ct})) ) \ \Rightarrow \ ( \mbox{open}(a,\mbox{cx},\mbox{ct})\mbox{ or }\mbox{equal\_sets}(a,\mbox{interior}(a,\mbox{cx},\mbox{ct})) )\qquad\mbox{cnf}(\mbox{problem\_9}_{145},\mbox{negated\_conjecture})$

$( \mbox{open}(a,\mbox{cx},\mbox{ct})\mbox{ and }\mbox{equal\_sets}(a,\mbox{interior}(a,\mbox{cx},\mbox{ct})) ) \ \Rightarrow \ ( \mbox{closed}(a,\mbox{cx},\mbox{ct})\mbox{ or }\mbox{equal\_sets}(a,\mbox{closure}(a,\mbox{cx},\mbox{ct})) )\qquad\mbox{cnf}(\mbox{problem\_9}_{146},\mbox{negated\_conjecture})$

$( \mbox{open}(a,\mbox{cx},\mbox{ct})\mbox{ and }\mbox{equal\_sets}(a,\mbox{interior}(a,\mbox{cx},\mbox{ct}))\mbox{ and }\mbox{closed}(a,\mbox{cx},\mbox{ct}) ) \ \Rightarrow \ \neg\,\mbox{equal\_sets}(a,\mbox{closure}(a,\mbox{cx},\mbox{ct}))\qquad\mbox{cnf}(\mbox{problem\_9}_{147},\mbox{negated\_conjecture})$

\medskip\textbf{TOP012-1.p} Intersections and finite unions of closed sets are closed






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{topological\_space}(\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_7}_{129},\mbox{negated\_conjecture})$

$( \mbox{closed}(\mbox{empty\_set},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{cx},\mbox{cx},\mbox{ct}) ) \ \Rightarrow \ ( \mbox{closed}(\mbox{cy}_1,\mbox{cx},\mbox{ct})\mbox{ or }\mbox{subset\_sets}(\mbox{union\_of\_members}(f),\mbox{cx}) )\qquad\mbox{cnf}(\mbox{problem\_7}_{130},\mbox{negated\_conjecture})$

$( \mbox{closed}(\mbox{empty\_set},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{cx},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{element\_of\_collection}(v,f) ) \ \Rightarrow \ ( \mbox{closed}(\mbox{cy}_1,\mbox{cx},\mbox{ct})\mbox{ or }\mbox{closed}(v,\mbox{cx},\mbox{ct}) )\qquad\mbox{cnf}(\mbox{problem\_7}_{131},\mbox{negated\_conjecture})$

$( \mbox{closed}(\mbox{empty\_set},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{cx},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{intersection\_of\_members}(f),\mbox{cx},\mbox{ct}) ) \ \Rightarrow \ \mbox{closed}(\mbox{cy}_1,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_7}_{132},\mbox{negated\_conjecture})$

$( \mbox{closed}(\mbox{empty\_set},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{cx},\mbox{cx},\mbox{ct}) ) \ \Rightarrow \ ( \mbox{closed}(\mbox{cy}_2,\mbox{cx},\mbox{ct})\mbox{ or }\mbox{subset\_sets}(\mbox{union\_of\_members}(f),\mbox{cx}) )\qquad\mbox{cnf}(\mbox{problem\_7}_{133},\mbox{negated\_conjecture})$

$( \mbox{closed}(\mbox{empty\_set},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{cx},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{element\_of\_collection}(v,f) ) \ \Rightarrow \ ( \mbox{closed}(\mbox{cy}_2,\mbox{cx},\mbox{ct})\mbox{ or }\mbox{closed}(v,\mbox{cx},\mbox{ct}) )\qquad\mbox{cnf}(\mbox{problem\_7}_{134},\mbox{negated\_conjecture})$

$( \mbox{closed}(\mbox{empty\_set},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{cx},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{intersection\_of\_members}(f),\mbox{cx},\mbox{ct}) ) \ \Rightarrow \ \mbox{closed}(\mbox{cy}_2,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_7}_{135},\mbox{negated\_conjecture})$

$( \mbox{closed}(\mbox{empty\_set},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{cx},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{union\_of\_sets}(\mbox{cy}_1,\mbox{cy}_2),\mbox{cx},\mbox{ct}) ) \ \Rightarrow \ \mbox{subset\_sets}(\mbox{union\_of\_members}(f),\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_7}_{136},\mbox{negated\_conjecture})$

$( \mbox{closed}(\mbox{empty\_set},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{cx},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{union\_of\_sets}(\mbox{cy}_1,\mbox{cy}_2),\mbox{cx},\mbox{ct})\mbox{ and }\mbox{element\_of\_collection}(v,f) ) \ \Rightarrow \ \mbox{closed}(v,\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_7}_{137},\mbox{negated\_conjecture})$

$( \mbox{closed}(\mbox{empty\_set},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{cx},\mbox{cx},\mbox{ct})\mbox{ and }\mbox{closed}(\mbox{union\_of\_sets}(\mbox{cy}_1,\mbox{cy}_2),\mbox{cx},\mbox{ct}) ) \ \Rightarrow \ \neg\,\mbox{closed}(\mbox{intersection\_of\_members}(f),\mbox{cx},\mbox{ct})\qquad\mbox{cnf}(\mbox{problem\_7}_{138},\mbox{negated\_conjecture})$

\medskip\textbf{TOP002-1.p} Topology generated by a basis forms a topological space, part 2






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{basis}(\mbox{cx},f)\qquad\mbox{cnf}(\mbox{lemma\_1b}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{element\_of\_collection}(\mbox{empty\_set},\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1b}_2,\mbox{negated\_conjecture})$

\medskip\textbf{TOP005-2.p} Topology generated by a basis forms a topological space, part 5






$\mbox{element\_of\_set}(u,\mbox{union\_of\_members}(\mbox{vf})) \ \Rightarrow \ \mbox{element\_of\_set}(u,f_1(\mbox{vf},u))\qquad\mbox{cnf}(\mbox{union\_of\_members}_1,\mbox{axiom})$

$\mbox{element\_of\_set}(u,\mbox{union\_of\_members}(\mbox{vf})) \ \Rightarrow \ \mbox{element\_of\_collection}(f_1(\mbox{vf},u),\mbox{vf})\qquad\mbox{cnf}(\mbox{union\_of\_members}_2,\mbox{axiom})$

$( \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ and }\mbox{element\_of\_set}(x,u) ) \ \Rightarrow \ \mbox{element\_of\_set}(x,f_{10}(\mbox{vf},u,x))\qquad\mbox{cnf}(\mbox{topology\_generated}_{37},\mbox{axiom})$

$( \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ and }\mbox{element\_of\_set}(x,u) ) \ \Rightarrow \ \mbox{element\_of\_collection}(f_{10}(\mbox{vf},u,x),\mbox{vf})\qquad\mbox{cnf}(\mbox{topology\_generated}_{38},\mbox{axiom})$

$( \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ and }\mbox{element\_of\_set}(x,u) ) \ \Rightarrow \ \mbox{subset\_sets}(f_{10}(\mbox{vf},u,x),u)\qquad\mbox{cnf}(\mbox{topology\_generated}_{39},\mbox{axiom})$

$\mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\mbox{ or }\mbox{element\_of\_set}(f_{11}(\mbox{vf},u),u)\qquad\mbox{cnf}(\mbox{topology\_generated}_{40},\mbox{axiom})$

$( \mbox{element\_of\_set}(f_{11}(\mbox{vf},u),\mbox{uu}_{11})\mbox{ and }\mbox{element\_of\_collection}(\mbox{uu}_{11},\mbox{vf})\mbox{ and }\mbox{subset\_sets}(\mbox{uu}_{11},u) ) \ \Rightarrow \ \mbox{element\_of\_collection}(u,\mbox{top\_of\_basis}(\mbox{vf}))\qquad\mbox{cnf}(\mbox{topology\_generated}_{41},\mbox{axiom})$

$\mbox{element\_of\_set}(u,x) \ \Rightarrow \ ( \mbox{subset\_sets}(x,y)\mbox{ or }\mbox{element\_of\_set}(u,y) )\qquad\mbox{cnf}(\mbox{set\_theory}_{19},\mbox{axiom})$

$( \mbox{subset\_sets}(x,y)\mbox{ and }\mbox{element\_of\_collection}(y,z) ) \ \Rightarrow \ \mbox{subset\_sets}(x,\mbox{union\_of\_members}(z))\qquad\mbox{cnf}(\mbox{set\_theory}_{20},\mbox{axiom})$

$( \mbox{subset\_collections}(x,y)\mbox{ and }\mbox{element\_of\_collection}(u,x) ) \ \Rightarrow \ \mbox{element\_of\_collection}(u,y)\qquad\mbox{cnf}(\mbox{set\_theory}_{21},\mbox{axiom})$

$\mbox{subset\_collections}(g,\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1e}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{element\_of\_collection}(\mbox{union\_of\_members}(g),\mbox{top\_of\_basis}(f))\qquad\mbox{cnf}(\mbox{lemma\_1e}_3,\mbox{negated\_conjecture})$

\medskip\textbf{TOP010-1.p} A finer topology induces a finer subspace topology






$\mbox{include}(\mbox{'Axioms/TOP001-0.ax'})$

$\mbox{finer}(\mbox{ct}_1,\mbox{ct}_2,\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_5}_{123},\mbox{negated\_conjecture})$

$\mbox{subset\_sets}(a,\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_5}_{124},\mbox{negated\_conjecture})$

$\neg\,\mbox{finer}(\mbox{subspace\_topology}(\mbox{cx},\mbox{ct}_1,a),\mbox{subspace\_topology}(\mbox{cx},\mbox{ct}_2,a),\mbox{cx})\qquad\mbox{cnf}(\mbox{problem\_5}_{125},\mbox{negated\_conjecture})$

\medskip\textbf{TOP022+1.p} Homotopy groups






$\forall a,b{:}\;( \mbox{isomorphic\_groups}(a,b)\iff \exists f{:}\;\mbox{a\_group\_isomorphism\_from\_to}(f,a,b) )\qquad\mbox{fof}(\mbox{isomorphic\_groups\_defn},\mbox{axiom})$

$\forall x,x_0,x_1{:}\;( \mbox{path\_connected}(x)\iff ( ( \mbox{a\_member\_of}(x_0,x)\mbox{ and }\mbox{a\_member\_of}(x_1,x) ) \ \Rightarrow \ \exists p{:}\;\mbox{a\_path\_from\_to\_in}(p,x_0,x_1,x) ) )\qquad\mbox{fof}(\mbox{path\_connected\_defn},\mbox{axiom})$

$\forall a,x_0,x_1,x{:}\;( \mbox{a\_path\_from\_to\_in}(a,x_0,x_1,x) \ \Rightarrow \ \mbox{a\_group\_isomorphism\_from\_to}(\mbox{alpha\_hat}(a),\mbox{first\_homotop\_grp}(x,x_0),\mbox{first\_homotop\_grp}(x,x_1)) )\qquad\mbox{fof}(\mbox{m\_8\_2}_1,\mbox{axiom})$

$\forall x,x_0,x_1{:}\;( ( \mbox{path\_connected}(x)\mbox{ and }\mbox{a\_member\_of}(x_0,x)\mbox{ and }\mbox{a\_member\_of}(x_1,x) ) \ \Rightarrow \ \mbox{isomorphic\_groups}(\mbox{first\_homotop\_grp}(x,x_0),\mbox{first\_homotop\_grp}(x,x_1)) )\qquad\mbox{fof}(\mbox{m\_8\_2}_2,\mbox{conjecture})$

\medskip
\end{document}