set S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #);
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 )
;
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
; verum