let L1, L2 be strict OrthoLattStr ; ( 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
; 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 for a, b being Element of L holds A . (a,b) = B . (a,b)let a,
b be
Element of
L;
A . (a,b) = B . (a,b)thus A . (
a,
b) =
a *' b
by A4
.=
B . (
a,
b)
by A7
;
verum end;
hence
L1 = L2
by A2, A3, A5, A6, BINOP_1:2; verum