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 a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of L1 . (a,b) = a9 _\/_ b9 & the L_meet of L1 . (a,b) = a9 _/\_ b9 ) ) & the carrier of L2 = IntervalSets U & ( for a, b being Element of the carrier of L2
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of L2 . (a,b) = a9 _\/_ b9 & the L_meet of L2 . (a,b) = a9 _/\_ b9 ) ) implies L1 = L2 )
assume that
A8: ( the carrier of L1 = IntervalSets U & ( for a, b being Element of the carrier of L1
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of L1 . (a,b) = a9 _\/_ b9 & the L_meet of L1 . (a,b) = a9 _/\_ b9 ) ) ) and
A9: ( the carrier of L2 = IntervalSets U & ( for a, b being Element of the carrier of L2
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of L2 . (a,b) = a9 _\/_ b9 & the L_meet of L2 . (a,b) = a9 _/\_ b9 ) ) ) ; :: thesis: L1 = L2
for a, b being Element of L1 holds the L_join of L1 . (a,b) = the L_join of L2 . (a,b)

proof

let a, b be Element of L1; :: thesis: the L_join of L1 . (a,b) = the L_join of L2 . (a,b)
reconsider a9 = a, b9 = b as non empty IntervalSet of U by A8, Def11;
the L_join of L1 . (a,b) = a9 _\/_ b9 by A8
.= the L_join of L2 . (a,b) by A9, A8 ;
hence the L_join of L1 . (a,b) = the L_join of L2 . (a,b) ; :: thesis: verum

end;

then A10: the L_join of L1 = the L_join of L2 by A8, A9, BINOP_1:2;
for a, b being Element of L1 holds the L_meet of L1 . (a,b) = the L_meet of L2 . (a,b)

proof

let a, b be Element of L1; :: thesis: the L_meet of L1 . (a,b) = the L_meet of L2 . (a,b)
reconsider a9 = a, b9 = b as non empty IntervalSet of U by A8, Def11;
the L_meet of L1 . (a,b) = a9 _/\_ b9 by A8
.= the L_meet of L2 . (a,b) by A8, A9 ;
hence the L_meet of L1 . (a,b) = the L_meet of L2 . (a,b) ; :: thesis: verum

end;

hence L1 = L2 by A8, A9, A10, BINOP_1:2; :: thesis: verum