let L be non empty reflexive LattRelStr ; :: thesis: ( L is trivial implies ( L is naturally_sup-generated & L is naturally_inf-generated ) )
assume L is trivial ; :: thesis: ( L is naturally_sup-generated & L is naturally_inf-generated )
then reconsider L' = L as non empty trivial reflexive LattRelStr ;
A1: L' is naturally_sup-generated

proof

for x, y being Element of L' holds
( x <= y iff x |_| y = y ) by STRUCT_0:def 10;
hence L' is naturally_sup-generated by Def10; :: thesis: verum

end;

L' is naturally_inf-generated

proof

for x, y being Element of L' holds
( x <= y iff x |^| y = x ) by STRUCT_0:def 10;
hence L' is naturally_inf-generated by Def11; :: thesis: verum

end;

hence ( L is naturally_sup-generated & L is naturally_inf-generated ) by A1; :: thesis: verum