set L = Normal_forms_on A;
let A1, A2 be strict LattStr ; :: thesis: ( the carrier of A1 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of A1 . (B,C) = mi (B \/ C) & the L_meet of A1 . (B,C) = mi (B ^ C) ) ) & the carrier of A2 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of A2 . (B,C) = mi (B \/ C) & the L_meet of A2 . (B,C) = mi (B ^ C) ) ) implies A1 = A2 )

assume that
A3: the carrier of A1 = Normal_forms_on A and
A4: for A, B being Element of Normal_forms_on A holds
( the L_join of A1 . (A,B) = mi (A \/ B) & the L_meet of A1 . (A,B) = mi (A ^ B) ) and
A5: the carrier of A2 = Normal_forms_on A and
A6: for A, B being Element of Normal_forms_on A holds
( the L_join of A2 . (A,B) = mi (A \/ B) & the L_meet of A2 . (A,B) = mi (A ^ B) ) ; :: thesis: A1 = A2
reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of () by A3, A5;
now :: thesis: for x, y being Element of Normal_forms_on A holds a1 . (x,y) = a2 . (x,y)
let x, y be Element of Normal_forms_on A; :: thesis: a1 . (x,y) = a2 . (x,y)
thus a1 . (x,y) = mi (x \/ y) by A4
.= a2 . (x,y) by A6 ; :: thesis: verum
end;
then A7: a1 = a2 ;
now :: thesis: for x, y being Element of Normal_forms_on A holds a3 . (x,y) = a4 . (x,y)
let x, y be Element of Normal_forms_on A; :: thesis: a3 . (x,y) = a4 . (x,y)
thus a3 . (x,y) = mi (x ^ y) by A4
.= a4 . (x,y) by A6 ; :: thesis: verum
end;
hence A1 = A2 by ; :: thesis: verum