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 L9 = L as non empty trivial reflexive LattRelStr ;
( ( for x, y being Element of L9 holds
( x <= y iff x |_| y = y ) ) & ( for x, y being Element of L9 holds
( x <= y iff x |^| y = x ) ) ) by STRUCT_0:def 10;
hence ( L is naturally_sup-generated & L is naturally_inf-generated ) by Def10, Def11; :: thesis: verum