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)

for a, b being Element of L1 holds the L_meet of L1 . (a,b) = the L_meet of L2 . (a,b)

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

then A10:
the L_join of L1 = the L_join of L2
by A8, A9, BINOP_1:2;
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;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

for a, b being Element of L1 holds the L_meet of L1 . (a,b) = the L_meet of L2 . (a,b)

proof

hence
L1 = L2
by A8, A9, A10, BINOP_1:2; :: thesis: verum
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;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