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 = y )

proof

let x, y be Element of S; :: thesis: ( x <= y iff x |_| y = y )
reconsider x' = x, y' = 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 9;
then x' [= y' by FILTER_1:32;
then x' |_| y' = y' by LATTICES:def 3;
hence x |_| y = y ; :: thesis: verum

end;

assume A1: x |_| y = y ; :: thesis: x <= y
x' |_| y' = x |_| y ;
then x' [= y' by A1, LATTICES:def 3;
then [x',y'] in LattRel L by FILTER_1:32;
hence x <= y by ORDERS_2:def 9; :: thesis: verum

end;

then A2: S is naturally_sup-generated by Def10;
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 x' = x, y' = 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 9;
then x' [= y' by FILTER_1:32;
then x' |^| y' = x' by LATTICES:21;
hence x |^| y = x ; :: thesis: verum

end;

assume A3: x |^| y = x ; :: thesis: x <= y
x' |^| y' = x |^| y ;
then x' [= y' by A3, LATTICES:21;
then [x',y'] in LattRel L by FILTER_1:32;
hence x <= y by ORDERS_2:def 9; :: thesis: verum

end;

then S is naturally_inf-generated by Def11;
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