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

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

hence
A1 = A2
by A5, A7, FUNCT_2:63; :: thesis: verum
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;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