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 the carrier 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 the carrier of A2
for y being Subset of 3 st x = y holds
the Compl of A2 . x = y ` ) implies A1 = A2 )
assume that
A0: ( LattStr(# the carrier of A1,the L_join of A1,the L_meet of A1 #) = latt B_6 & ( for x being Element of the carrier of A1
for y being Subset of 3 st x = y holds
the Compl of A1 . x = y ` ) ) and
A2: ( LattStr(# the carrier of A2,the L_join of A2,the L_meet of A2 #) = latt B_6 & ( for x being Element of the carrier of A2
for y being Subset of 3 st x = y holds
the Compl of A2 . x = y ` ) ) ; :: thesis: A1 = A2
set M = the carrier of A1;
set f1 = the Compl of A1;
set f2 = the Compl of A2;
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 A0, CosikX1;
thus the Compl of A1 . x = y ` by A0
.= the Compl of A2 . x by A2, A0 ; :: thesis: verum

end;

hence A1 = A2 by A0, A2, FUNCT_2:113; :: thesis: verum