let L be non empty LattRelStr ; :: thesis: ( L is naturally_sup-generated & L is Lattice-like implies ( L is with_infima & L is with_suprema ) )
assume ( L is naturally_sup-generated & L is Lattice-like ) ; :: thesis: ( L is with_infima & L is with_suprema )
then reconsider L9 = L as non empty Lattice-like naturally_sup-generated LattRelStr ;
( LattPOSet L9 is with_suprema & LattPOSet L9 is with_infima ) ;
then ( RelStr(# the carrier of L9, the InternalRel of L9 #) is with_suprema & RelStr(# the carrier of L9, the InternalRel of L9 #) is with_infima ) by Th23;
hence ( L is with_infima & L is with_suprema ) by YELLOW_7:14, YELLOW_7:15; :: thesis: verum