set S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #);
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;
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;
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;
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
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;
A5: for a, b being Element of 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 ) ;
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;
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;
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;
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 b1 being SubLattice of L st b1 is strict ; :: thesis: verum