A1: 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 () & b in the carrier of () ) ;
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 ; :: thesis: verum
end;
A2: 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 () & b in the carrier of () & c in the carrier of () ) ;
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 () & ab in the carrier of () ) by Def12;
a "\/" (b "\/" c) = the L_join of () . (a,bc) by Def12
.= a9 _\/_ bc by
.= (a9 _\/_ b9) _\/_ c9 by Th23
.= the L_join of () . (ab,c9) by
.= (a "\/" b) "\/" c by Def12 ;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; :: thesis: verum
end;
hence InterLatt U is join-associative ; :: thesis: verum
end;
A4: 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 () & b in the carrier of () ) ;
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 () by Def12;
(a "/\" b) "\/" b = the L_join of () . (ab,b) by Def12
.= ab _\/_ b9 by
.= b by Th36 ;
hence (a "/\" b) "\/" b = b ; :: thesis: verum
end;
hence InterLatt U is meet-absorbing ; :: thesis: verum
end;
A6: 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 () & b in the carrier of () & c in the carrier of () ) ;
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 () & ab in the carrier of () ) by Def12;
a "/\" (b "/\" c) = the L_meet of () . (a,bc) by Def12
.= a9 _/\_ bc by
.= (a9 _/\_ b9) _/\_ c9 by Th24
.= the L_meet of () . (ab,c9) by
.= (a "/\" b) "/\" c by Def12 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum
end;
hence InterLatt U is meet-associative ; :: thesis: verum
end;
A8: InterLatt U is join-absorbing
proof
for a, b being Element of the carrier of () holds a "/\" (a "\/" b) = a
proof
let a, b be Element of the carrier of (); :: thesis: a "/\" (a "\/" b) = a
( a in the carrier of () & b in the carrier of () ) ;
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 () by Def12;
a "/\" (a "\/" b) = the L_meet of () . (a9,(a9 _\/_ b9)) by Def12
.= a9 _/\_ ab by
.= a by Th35 ;
hence a "/\" (a "\/" b) = a ; :: thesis: verum
end;
hence InterLatt U is join-absorbing ; :: thesis: verum
end;
InterLatt U is meet-commutative
proof
for a, b being Element of the carrier of () holds a "/\" b = b "/\" a
proof
let a, b be Element of the carrier of (); :: thesis: a "/\" b = b "/\" a
( a in the carrier of () & b in the carrier of () ) ;
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 () . (a,b) = b9 _/\_ a9 by Def12
.= the L_meet of () . (b,a) by Def12 ;
hence a "/\" b = b "/\" a ; :: thesis: verum
end;
hence InterLatt U is meet-commutative ; :: thesis: verum
end;
hence InterLatt U is Lattice-like by A1, A2, A4, A6, A8; :: thesis: verum