set R = LattRel L;
set S = LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #);
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #), the L_join of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #), the L_meet of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #) #) ;
then reconsider S = LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #) as LatAugmentation of L by Def9;
for x, y being Element of S holds
( x <= y iff x |^| y = x )

proof

let x, y be Element of S; :: thesis: ( x <= y iff x |^| y = x )
reconsider x9 = x, y9 = y as Element of L ;

hereby :: thesis: ( x |^| y = x implies x <= y )

assume x <= y ; :: thesis: x |^| y = x
then [x,y] in the InternalRel of S by ORDERS_2:def 5;
then x9 [= y9 by FILTER_1:31;
then x9 |^| y9 = x9 by LATTICES:4;
hence x |^| y = x ; :: thesis: verum

end;

A1: x9 |^| y9 = x |^| y ;
assume x |^| y = x ; :: thesis: x <= y
then x9 [= y9 by A1, LATTICES:4;
then [x9,y9] in LattRel L by FILTER_1:31;
hence x <= y by ORDERS_2:def 5; :: thesis: verum

end;

then A2: S is naturally_inf-generated ;
for x, y being Element of S holds
( x <= y iff x |_| y = y )

proof

let x, y be Element of S; :: thesis: ( x <= y iff x |_| y = y )
reconsider x9 = x, y9 = y as Element of L ;

hereby :: thesis: ( x |_| y = y implies x <= y )

assume x <= y ; :: thesis: x |_| y = y
then [x,y] in the InternalRel of S by ORDERS_2:def 5;
then x9 [= y9 by FILTER_1:31;
then x9 |_| y9 = y9 ;
hence x |_| y = y ; :: thesis: verum

end;

assume x |_| y = y ; :: thesis: x <= y
then x9 [= y9 ;
then [x9,y9] in LattRel L by FILTER_1:31;
hence x <= y by ORDERS_2:def 5; :: thesis: verum

end;

then S is naturally_sup-generated ;
hence ex b₁ being LatAugmentation of L st
( b₁ is naturally_sup-generated & b₁ is naturally_inf-generated & b₁ is Lattice-like ) by A2; :: thesis: verum