let L be 1 -element reflexive LattRelStr ; :: thesis: ( L is naturally_sup-generated & L is naturally_inf-generated )
reconsider L9 = L as 1 -element 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 ) ; :: thesis: verum