let y, x be LD-EqClass; :: thesis: ( ex t being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf ('not' t) ) implies ex t being GRZ-formula st
( y = LD-EqClassOf t & x = LD-EqClassOf ('not' t) ) )
given t being GRZ-formula such that A1: x = LD-EqClassOf t and
A2: y = LD-EqClassOf ('not' t) ; :: thesis: ex t being GRZ-formula st
( y = LD-EqClassOf t & x = LD-EqClassOf ('not' t) )
set u = 'not' t;
('not' ('not' t)) '=' t is LD-provable ;
then x = LD-EqClassOf ('not' ('not' t)) by A1, Def76, Th80;
hence ex t being GRZ-formula st
( y = LD-EqClassOf t & x = LD-EqClassOf ('not' t) ) by A2; :: thesis: verum