let L1, L2 be non empty strict LattStr ; ( 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
A1:
( 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
A2:
( 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 ) ) )
; 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;
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 A1, DefAG;
the
L_join of
L1 . a,
b =
a9 _\/_ b9
by A1
.=
the
L_join of
L2 . a,
b
by A2, A1
;
hence
the
L_join of
L1 . a,
b = the
L_join of
L2 . a,
b
;
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 L1 holds the L_meet of L1 . a,b = the L_meet of L2 . a,b
proof
let a,
b be
Element of
L1;
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 A1, DefAG;
the
L_meet of
L1 . a,
b =
a9 _/\_ b9
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
;
verum
end;
hence
L1 = L2
by A1, A2, Z1, BINOP_1:2; verum