let L1, L2 be strict OrthoLattStr ; :: thesis: ( the carrier of L1 = the carrier of L & the L_join of L1 = the L_join of L & the Compl of L1 = the Compl of L & ( for a, b being Element of L holds the L_meet of L1 . (a,b) = a *' b ) & the carrier of L2 = the carrier of L & the L_join of L2 = the L_join of L & the Compl of L2 = the Compl of L & ( for a, b being Element of L holds the L_meet of L2 . (a,b) = a *' b ) implies L1 = L2 )
assume that
A2: the carrier of L1 = the carrier of L and
A3: ( the L_join of L1 = the L_join of L & the Compl of L1 = the Compl of L ) and
A4: for a, b being Element of L holds the L_meet of L1 . (a,b) = a *' b and
A5: the carrier of L2 = the carrier of L and
A6: ( the L_join of L2 = the L_join of L & the Compl of L2 = the Compl of L ) and
A7: for a, b being Element of L holds the L_meet of L2 . (a,b) = a *' b ; :: thesis: L1 = L2
reconsider A = the L_meet of L1, B = the L_meet of L2 as BinOp of the carrier of L by A2, A5;

now :: thesis: for a, b being Element of L holds A . (a,b) = B . (a,b)

let a, b be Element of L; :: thesis: A . (a,b) = B . (a,b)
thus A . (a,b) = a *' b by A4
.= B . (a,b) by A7 ; :: thesis: verum

end;

hence L1 = L2 by A2, A3, A5, A6, BINOP_1:2; :: thesis: verum