Step * of Lemma topeq_weakening

X:Space. ∀a,b:|X|.  ((a b ∈ |X|)  topeq(X;a;b))
BY
((InstLemma `topeq-equiv` [] THEN ParallelLast') THEN -1 THEN Auto) }


Latex:


Latex:
\mforall{}X:Space.  \mforall{}a,b:|X|.    ((a  =  b)  {}\mRightarrow{}  topeq(X;a;b))


By


Latex:
((InstLemma  `topeq-equiv`  []  THEN  ParallelLast')  THEN  D  -1  THEN  Auto)




Home Index