set S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #);

for a9, b9 being Element of L st a = a9 & b = b9 holds

( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 ) ;

then reconsider S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) as Lattice ;

( the L_join of S = the L_join of L || the carrier of S & the L_meet of S = the L_meet of L || the carrier of S ) by RELSET_1:19;

then S is SubLattice of L by Def12;

hence ex b_{1} being SubLattice of L st b_{1} is strict
; :: thesis: verum

A1: now :: thesis: for a, b, c being Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

let a, b, c be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c

reconsider a9 = a, b9 = b, c9 = c as Element of L ;

thus a "\/" (b "\/" c) = a9 "\/" (b9 "\/" c9)

.= (a9 "\/" b9) "\/" c9 by LATTICES:def 5

.= (a "\/" b) "\/" c ; :: thesis: verum

end;reconsider a9 = a, b9 = b, c9 = c as Element of L ;

thus a "\/" (b "\/" c) = a9 "\/" (b9 "\/" c9)

.= (a9 "\/" b9) "\/" c9 by LATTICES:def 5

.= (a "\/" b) "\/" c ; :: thesis: verum

A2: now :: thesis: for a, b being Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) holds (a "/\" b) "\/" b = b

let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); :: thesis: (a "/\" b) "\/" b = b

reconsider a9 = a, b9 = b as Element of L ;

thus (a "/\" b) "\/" b = (a9 "/\" b9) "\/" b9

.= b by LATTICES:def 8 ; :: thesis: verum

end;reconsider a9 = a, b9 = b as Element of L ;

thus (a "/\" b) "\/" b = (a9 "/\" b9) "\/" b9

.= b by LATTICES:def 8 ; :: thesis: verum

A3: now :: thesis: for a, b being Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) holds a "/\" (a "\/" b) = a

let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); :: thesis: a "/\" (a "\/" b) = a

reconsider a9 = a, b9 = b as Element of L ;

thus a "/\" (a "\/" b) = a9 "/\" (a9 "\/" b9)

.= a by LATTICES:def 9 ; :: thesis: verum

end;reconsider a9 = a, b9 = b as Element of L ;

thus a "/\" (a "\/" b) = a9 "/\" (a9 "\/" b9)

.= a by LATTICES:def 9 ; :: thesis: verum

A4: now :: thesis: for a, b, c being Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

A5:
for a, b being Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #)let a, b, c be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c

reconsider a9 = a, b9 = b, c9 = c as Element of L ;

thus a "/\" (b "/\" c) = a9 "/\" (b9 "/\" c9)

.= (a9 "/\" b9) "/\" c9 by LATTICES:def 7

.= (a "/\" b) "/\" c ; :: thesis: verum

end;reconsider a9 = a, b9 = b, c9 = c as Element of L ;

thus a "/\" (b "/\" c) = a9 "/\" (b9 "/\" c9)

.= (a9 "/\" b9) "/\" c9 by LATTICES:def 7

.= (a "/\" b) "/\" c ; :: thesis: verum

for a9, b9 being Element of L st a = a9 & b = b9 holds

( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 ) ;

A6: now :: thesis: for a, b being Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) holds a "/\" b = b "/\" a

let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); :: thesis: a "/\" b = b "/\" a

reconsider a9 = a, b9 = b as Element of L ;

thus a "/\" b = b9 "/\" a9 by A5

.= b "/\" a ; :: thesis: verum

end;reconsider a9 = a, b9 = b as Element of L ;

thus a "/\" b = b9 "/\" a9 by A5

.= b "/\" a ; :: thesis: verum

now :: thesis: for a, b being Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) holds a "\/" b = b "\/" a

then
( LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is join-commutative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is join-associative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is meet-absorbing & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is meet-commutative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is meet-associative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is join-absorbing )
by A1, A2, A6, A4, A3;let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); :: thesis: a "\/" b = b "\/" a

reconsider a9 = a, b9 = b as Element of L ;

thus a "\/" b = b9 "\/" a9 by A5

.= b "\/" a ; :: thesis: verum

end;reconsider a9 = a, b9 = b as Element of L ;

thus a "\/" b = b9 "\/" a9 by A5

.= b "\/" a ; :: thesis: verum

then reconsider S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) as Lattice ;

( the L_join of S = the L_join of L || the carrier of S & the L_meet of S = the L_meet of L || the carrier of S ) by RELSET_1:19;

then S is SubLattice of L by Def12;

hence ex b