consider t being GRZ-formula such that
A2: x = LD-EqClassOf t by Th88;
take LD-EqClassOf ('not' t) ; :: thesis: ex t being GRZ-formula st
( x = LD-EqClassOf t & LD-EqClassOf ('not' t) = LD-EqClassOf ('not' t) )
thus ex t being GRZ-formula st
( x = LD-EqClassOf t & LD-EqClassOf ('not' t) = LD-EqClassOf ('not' t) ) by A2; :: thesis: verum