let A1, A2 be strict OrthoLattStr ; :: thesis: ( LattStr(# the carrier of A1, the L_join of A1, the L_meet of A1 #) = latt B_6 & ( for x being Element of A1
for y being Subset of 3 st x = y holds
the Compl of A1 . x = y ` ) & LattStr(# the carrier of A2, the L_join of A2, the L_meet of A2 #) = latt B_6 & ( for x being Element of A2
for y being Subset of 3 st x = y holds
the Compl of A2 . x = y ` ) implies A1 = A2 )
assume that
A5: LattStr(# the carrier of A1, the L_join of A1, the L_meet of A1 #) = latt B_6 and
A6: for x being Element of A1
for y being Subset of 3 st x = y holds
the Compl of A1 . x = y ` and
A7: LattStr(# the carrier of A2, the L_join of A2, the L_meet of A2 #) = latt B_6 and
A8: for x being Element of A2
for y being Subset of 3 st x = y holds
the Compl of A2 . x = y ` ; :: thesis: A1 = A2
set f2 = the Compl of A2;
set f1 = the Compl of A1;
set M = the carrier of A1;
for x being Element of the carrier of A1 holds the Compl of A1 . x = the Compl of A2 . x

proof

let x be Element of the carrier of A1; :: thesis: the Compl of A1 . x = the Compl of A2 . x
reconsider y = x as Subset of 3 by A5, Th8;
thus the Compl of A1 . x = y ` by A6
.= the Compl of A2 . x by A5, A7, A8 ; :: thesis: verum

end;

hence A1 = A2 by A5, A7, FUNCT_2:63; :: thesis: verum