set S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #);
( the L_join of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = the L_join of L || the carrier of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & the L_meet of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = the L_meet of L || the carrier of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ) ;
then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is SubLattStr of L by Defx1;
hence ex b₁ being SubLattStr of L st b₁ is strict ; :: thesis: verum