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

A1: now

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 a' = a, b' = b, c' = c as Element of L ;
thus a "\/" (b "\/" c) = a' "\/" (b' "\/" c')
.= (a' "\/" b') "\/" c' by LATTICES:def 5
.= (a "\/" b) "\/" c ; :: thesis: verum

end;

A2: now

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 a' = a, b' = b as Element of L ;
thus (a "/\" b) "\/" b = (a' "/\" b') "\/" b'
.= b by LATTICES:def 8 ; :: thesis: verum

end;

A3: now

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 a' = a, b' = b as Element of L ;
thus a "/\" (a "\/" b) = a' "/\" (a' "\/" b')
.= a by LATTICES:def 9 ; :: thesis: verum

end;

A4: now

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 a' = a, b' = b, c' = c as Element of L ;
thus a "/\" (b "/\" c) = a' "/\" (b' "/\" c')
.= (a' "/\" b') "/\" c' 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 a', b' being Element of L st a = a' & b = b' holds
( a "\/" b = a' "\/" b' & a "/\" b = a' "/\" b' ) ;

A6: now

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 a' = a, b' = b as Element of L ;
thus a "/\" b = b' "/\" a' by A5
.= b "/\" a ; :: thesis: verum

end;

now

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 a' = a, b' = b as Element of L ;
thus a "\/" b = b' "\/" a' 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, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
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:34;
then S is SubLattice of L by Def16;
hence ex b₁ being SubLattice of L st b₁ is strict ; :: thesis: verum