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 & 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 ) ) and
A3: ( 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 ) ) ; :: 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, A3;

now

let a, b be Element of L; :: thesis: A . a,b = B . a,b
thus A . a,b = a *' b by A2
.= B . a,b by A3 ; :: thesis: verum

end;

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