let y1, y2 be LD-EqClass; :: thesis: ( ex t being GRZ-formula st
( x = LD-EqClassOf t & y1 = LD-EqClassOf ('not' t) ) & ex t being GRZ-formula st
( x = LD-EqClassOf t & y2 = LD-EqClassOf ('not' t) ) implies y1 = y2 )
given t1 being GRZ-formula such that A1: x = LD-EqClassOf t1 and
A2: y1 = LD-EqClassOf ('not' t1) ; :: thesis: ( for t being GRZ-formula holds
( not x = LD-EqClassOf t or not y2 = LD-EqClassOf ('not' t) ) or y1 = y2 )
given t2 being GRZ-formula such that A3: x = LD-EqClassOf t2 and
A4: y2 = LD-EqClassOf ('not' t2) ; :: thesis: y1 = y2
t1 LD-= t2 by A1, A3, Th80;
hence y1 = y2 by A2, A4, Th76, Th80; :: thesis: verum