A1:
InterLatt U is join-commutative

proof

A2:
InterLatt U is join-associative
for a, b being Element of (InterLatt U) holds a "\/" b = b "\/" a

end;proof

hence
InterLatt U is join-commutative
; :: thesis: verum
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;( 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

proof

A4:
InterLatt U is meet-absorbing
for a, b, c being Element of (InterLatt U) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

end;proof

hence
InterLatt U is join-associative
; :: thesis: verum
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;( 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

proof

A6:
InterLatt U is meet-associative
for a, b being Element of (InterLatt U) holds (a "/\" b) "\/" b = b

end;proof

hence
InterLatt U is meet-absorbing
; :: thesis: verum
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;( 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

proof

A8:
InterLatt U is join-absorbing
for a, b, c being Element of (InterLatt U) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

end;proof

hence
InterLatt U is meet-associative
; :: thesis: verum
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;( 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

proof

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

end;proof

hence
InterLatt U is join-absorbing
; :: thesis: verum
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;( 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

proof

hence
InterLatt U is Lattice-like
by A1, A2, A4, A6, A8; :: thesis: verum
for a, b being Element of the carrier of (InterLatt U) holds a "/\" b = b "/\" a

end;proof

hence
InterLatt U is meet-commutative
; :: thesis: verum
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;( 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