let L1, L2 be non empty strict LattStr ; :: thesis: ( the carrier of L1 = IntervalSets U & ( for a, b being Element of the carrier of L1
for a', b' being non empty IntervalSet of U st a' = a & b' = b holds
( the L_join of L1 . a,b = a' _\/_ b' & the L_meet of L1 . a,b = a' _/\_ b' ) ) & the carrier of L2 = IntervalSets U & ( for a, b being Element of the carrier of L2
for a', b' being non empty IntervalSet of U st a' = a & b' = b holds
( the L_join of L2 . a,b = a' _\/_ b' & the L_meet of L2 . a,b = a' _/\_ b' ) ) implies L1 = L2 )
assume that
A1: ( the carrier of L1 = IntervalSets U & ( for a, b being Element of the carrier of L1
for a', b' being non empty IntervalSet of U st a' = a & b' = b holds
( the L_join of L1 . a,b = a' _\/_ b' & the L_meet of L1 . a,b = a' _/\_ b' ) ) ) and
A2: ( the carrier of L2 = IntervalSets U & ( for a, b being Element of the carrier of L2
for a', b' being non empty IntervalSet of U st a' = a & b' = b holds
( the L_join of L2 . a,b = a' _\/_ b' & the L_meet of L2 . a,b = a' _/\_ b' ) ) ) ; :: thesis: L1 = L2
for a, b being Element of holds the L_join of L1 . a,b = the L_join of L2 . a,b

proof

let a, b be Element of ; :: thesis: the L_join of L1 . a,b = the L_join of L2 . a,b
reconsider a' = a, b' = b as non empty IntervalSet of U by A1, DefAG;
B3: the L_join of L1 . a,b = a' _\/_ b' by A1
.= the L_join of L2 . a,b by A2, A1 ;
thus the L_join of L1 . a,b = the L_join of L2 . a,b by B3; :: thesis: verum

end;

then Z1: the L_join of L1 = the L_join of L2 by A1, A2, BINOP_1:2;
for a, b being Element of holds the L_meet of L1 . a,b = the L_meet of L2 . a,b

proof

let a, b be Element of ; :: thesis: the L_meet of L1 . a,b = the L_meet of L2 . a,b
reconsider a' = a, b' = b as non empty IntervalSet of U by A1, DefAG;
the L_meet of L1 . a,b = a' _/\_ b' by A1
.= the L_meet of L2 . a,b by A1, A2 ;
hence the L_meet of L1 . a,b = the L_meet of L2 . a,b ; :: thesis: verum

end;

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