let A1, A2 be strict LattStr ; :: thesis: ( the carrier of A1 = SubstitutionSet V,C & ( for A, B being Element of SubstitutionSet V,C holds
( the L_join of A1 . A,B = mi (A \/ B) & the L_meet of A1 . A,B = mi (A ^ B) ) ) & the carrier of A2 = SubstitutionSet V,C & ( for A, B being Element of SubstitutionSet V,C holds
( the L_join of A2 . A,B = mi (A \/ B) & the L_meet of A2 . A,B = mi (A ^ B) ) ) implies A1 = A2 )
assume that
A3: the carrier of A1 = SubstitutionSet V,C and
A4: for A, B being Element of SubstitutionSet V,C 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 = SubstitutionSet V,C and
A6: for A, B being Element of SubstitutionSet V,C 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 (SubstitutionSet V,C) by A3, A5;

now

let x, y be Element of SubstitutionSet V,C; :: 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 by BINOP_1:2;

now

let x, y be Element of SubstitutionSet V,C; :: 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 A3, A5, A7, BINOP_1:2; :: thesis: verum