A1: InterLatt U is join-commutative

proof

for a, b being Element of (InterLatt U) holds a "\/" b = b "\/" a

proof

let a, b be Element of (InterLatt U); :: thesis: a "\/" b = b "\/" a
( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) ) ;
then ( a in IntervalSets U & b in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
a "\/" b = a9 _\/_ b9 by Def12
.= b9 _\/_ a9
.= b "\/" a by Def12 ;
hence a "\/" b = b "\/" a ; :: thesis: verum

end;

hence InterLatt U is join-commutative by LATTICES:def 4; :: thesis: verum

end;

A2: InterLatt U is join-associative

proof

for a, b, c being Element of (InterLatt U) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof

let a, b, c be Element of (InterLatt U); :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) & c in the carrier of (InterLatt U) ) ;
then ( a in IntervalSets U & b in IntervalSets U & c in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U by Def11;
reconsider bc = b9 _\/_ c9 as non empty IntervalSet of U ;
reconsider ab = a9 _\/_ b9 as non empty IntervalSet of U ;
( bc in IntervalSets U & ab in IntervalSets U ) by Def11;
then A3: ( bc in the carrier of (InterLatt U) & ab in the carrier of (InterLatt U) ) by Def12;
a "\/" (b "\/" c) = the L_join of (InterLatt U) . (a,bc) by Def12
.= a9 _\/_ bc by Def12, A3
.= (a9 _\/_ b9) _\/_ c9 by Th23
.= the L_join of (InterLatt U) . (ab,c9) by Def12, A3
.= (a "\/" b) "\/" c by Def12 ;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; :: thesis: verum

end;

hence InterLatt U is join-associative by LATTICES:def 5; :: thesis: verum

end;

A4: InterLatt U is meet-absorbing

proof

for a, b being Element of (InterLatt U) holds (a "/\" b) "\/" b = b

proof

let a, b be Element of (InterLatt U); :: thesis: (a "/\" b) "\/" b = b
( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) ) ;
then ( a in IntervalSets U & b in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
reconsider ab = a9 _/\_ b9 as non empty IntervalSet of U ;
ab in IntervalSets U by Def11;
then A5: ab in the carrier of (InterLatt U) by Def12;
(a "/\" b) "\/" b = the L_join of (InterLatt U) . (ab,b) by Def12
.= ab _\/_ b9 by Def12, A5
.= b by Th36 ;
hence (a "/\" b) "\/" b = b ; :: thesis: verum

end;

hence InterLatt U is meet-absorbing by LATTICES:def 8; :: thesis: verum

end;

A6: InterLatt U is meet-associative

proof

for a, b, c being Element of (InterLatt U) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof

let a, b, c be Element of (InterLatt U); :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) & c in the carrier of (InterLatt U) ) ;
then ( a in IntervalSets U & b in IntervalSets U & c in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U by Def11;
reconsider bc = b9 _/\_ c9, ab = a9 _/\_ b9 as non empty IntervalSet of U ;
( bc in IntervalSets U & ab in IntervalSets U ) by Def11;
then A7: ( bc in the carrier of (InterLatt U) & ab in the carrier of (InterLatt U) ) by Def12;
a "/\" (b "/\" c) = the L_meet of (InterLatt U) . (a,bc) by Def12
.= a9 _/\_ bc by Def12, A7
.= (a9 _/\_ b9) _/\_ c9 by Th24
.= the L_meet of (InterLatt U) . (ab,c9) by Def12, A7
.= (a "/\" b) "/\" c by Def12 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum

end;

hence InterLatt U is meet-associative by LATTICES:def 7; :: thesis: verum

end;

A8: InterLatt U is join-absorbing

proof

for a, b being Element of the carrier of (InterLatt U) holds a "/\" (a "\/" b) = a

proof

let a, b be Element of the carrier of (InterLatt U); :: thesis: a "/\" (a "\/" b) = a
( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) ) ;
then ( a in IntervalSets U & b in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
reconsider ab = a9 _\/_ b9 as non empty IntervalSet of U ;
ab in IntervalSets U by Def11;
then A9: ab in the carrier of (InterLatt U) by Def12;
a "/\" (a "\/" b) = the L_meet of (InterLatt U) . (a9,(a9 _\/_ b9)) by Def12
.= a9 _/\_ ab by Def12, A9
.= a by Th35 ;
hence a "/\" (a "\/" b) = a ; :: thesis: verum

end;

hence InterLatt U is join-absorbing by LATTICES:def 9; :: thesis: verum

end;

InterLatt U is meet-commutative

proof

for a, b being Element of the carrier of (InterLatt U) holds a "/\" b = b "/\" a

proof

let a, b be Element of the carrier of (InterLatt U); :: thesis: a "/\" b = b "/\" a
( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) ) ;
then ( a in IntervalSets U & b in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
a9 _/\_ b9 = b9 _/\_ a9 ;
then the L_meet of (InterLatt U) . (a,b) = b9 _/\_ a9 by Def12
.= the L_meet of (InterLatt U) . (b,a) by Def12 ;
hence a "/\" b = b "/\" a ; :: thesis: verum

end;

hence InterLatt U is meet-commutative by LATTICES:def 6; :: thesis: verum

end;

hence InterLatt U is Lattice-like by A1, A2, A4, A6, A8; :: thesis: verum