Step * of Lemma Sierpinski-cases

[x:Sierpinski]. ((¬(x = ⊤ ∈ Sierpinski)) ∧ (x = ⊥ ∈ Sierpinski))))
BY
TACTIC:(Auto THEN THEN Auto THEN FLemma `not-Sierpinski-top` [-2] THEN Auto) }


Latex:


Latex:
\mforall{}[x:Sierpinski].  (\mneg{}((\mneg{}(x  =  \mtop{}))  \mwedge{}  (\mneg{}(x  =  \mbot{}))))


By


Latex:
TACTIC:(Auto  THEN  D  0  THEN  Auto  THEN  FLemma  `not-Sierpinski-top`  [-2]  THEN  Auto)




Home Index