a0: InterLatt U is join-commutative

proof

for a, b being Element of holds a "\/" b = b "\/" a

proof

let a, b be Element of ; :: 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 a' = a, b' = b as non empty IntervalSet of U by DefAG;
a "\/" b = a' _\/_ b' by DefLLL
.= b' _\/_ a'
.= 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 holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof

let a, b, c be Element of ; :: 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 a' = a, b' = b, c' = c as non empty IntervalSet of U by DefAG;
reconsider bc = b' _\/_ c' as non empty IntervalSet of U ;
reconsider ab = a' _\/_ b' 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
.= a' _\/_ bc by DefLLL, Y
.= (a' _\/_ b') _\/_ c' by Asso1
.= the L_join of (InterLatt U) . ab,c' 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 holds (a "/\" b) "\/" b = b

proof

let a, b be Element of ; :: 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 a' = a, b' = b as non empty IntervalSet of U by DefAG;
reconsider ab = a' _/\_ b' 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 _\/_ b' 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 holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof

let a, b, c be Element of ; :: 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 a' = a, b' = b, c' = c as non empty IntervalSet of U by DefAG;
reconsider bc = b' _/\_ c', ab = a' _/\_ b' 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
.= a' _/\_ bc by DefLLL, Y
.= (a' _/\_ b') _/\_ c' by Prz1
.= the L_meet of (InterLatt U) . ab,c' 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 a' = a, b' = b as non empty IntervalSet of U by DefAG;
reconsider ab = a' _\/_ b' 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) . a',(a' _\/_ b') by DefLLL
.= a' _/\_ 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 a' = a, b' = b as non empty IntervalSet of U by DefAG;
a' _/\_ b' = b' _/\_ a' ;
then the L_meet of (InterLatt U) . a,b = b' _/\_ a' 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