a0: 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 DefLLL;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by DefAG;
a "\/" b = a9 _\/_ b9 by DefLLL
.= b9 _\/_ a9
.= b "\/" a by DefLLL ;
hence a "\/" b = b "\/" a ; :: thesis: verum

end;

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

end;

a1: 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 DefLLL;
then reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U by DefAG;
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 DefAG;
then Y: ( bc in the carrier of (InterLatt U) & ab in the carrier of (InterLatt U) ) by DefLLL;
a "\/" (b "\/" c) = the L_join of (InterLatt U) . a,bc by DefLLL
.= a9 _\/_ bc by DefLLL, Y
.= (a9 _\/_ b9) _\/_ c9 by Asso1
.= the L_join of (InterLatt U) . ab,c9 by DefLLL, Y
.= (a "\/" b) "\/" c by DefLLL ;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; :: thesis: verum

end;

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

end;

a2: 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 DefLLL;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by DefAG;
reconsider ab = a9 _/\_ b9 as non empty IntervalSet of U ;
ab in IntervalSets U by DefAG;
then Y: ab in the carrier of (InterLatt U) by DefLLL;
(a "/\" b) "\/" b = the L_join of (InterLatt U) . ab,b by DefLLL
.= ab _\/_ b9 by DefLLL, Y
.= b by Abs2 ;
hence (a "/\" b) "\/" b = b ; :: thesis: verum

end;

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

end;

a3: 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 DefLLL;
then reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U by DefAG;
reconsider bc = b9 _/\_ c9, ab = a9 _/\_ b9 as non empty IntervalSet of U ;
( bc in IntervalSets U & ab in IntervalSets U ) by DefAG;
then Y: ( bc in the carrier of (InterLatt U) & ab in the carrier of (InterLatt U) ) by DefLLL;
a "/\" (b "/\" c) = the L_meet of (InterLatt U) . a,bc by DefLLL
.= a9 _/\_ bc by DefLLL, Y
.= (a9 _/\_ b9) _/\_ c9 by Prz1
.= the L_meet of (InterLatt U) . ab,c9 by DefLLL, Y
.= (a "/\" b) "/\" c by DefLLL ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum

end;

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

end;

a4: 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 DefLLL;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by DefAG;
reconsider ab = a9 _\/_ b9 as non empty IntervalSet of U ;
ab in IntervalSets U by DefAG;
then X: ab in the carrier of (InterLatt U) by DefLLL;
a "/\" (a "\/" b) = the L_meet of (InterLatt U) . a9,(a9 _\/_ b9) by DefLLL
.= a9 _/\_ ab by DefLLL, X
.= a by Abs1 ;
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 DefLLL;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by DefAG;
a9 _/\_ b9 = b9 _/\_ a9 ;
then the L_meet of (InterLatt U) . a,b = b9 _/\_ a9 by DefLLL
.= the L_meet of (InterLatt U) . b,a by DefLLL ;
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 a0, a1, a2, a3, a4; :: thesis: verum