set S = the non empty full sups-inheriting SubRelStr of L;
take the non empty full sups-inheriting SubRelStr of L ; :: thesis: ( not the non empty full sups-inheriting SubRelStr of L is empty & the non empty full sups-inheriting SubRelStr of L is sups-inheriting & the non empty full sups-inheriting SubRelStr of L is finite-sups-inheriting & the non empty full sups-inheriting SubRelStr of L is bottom-inheriting & the non empty full sups-inheriting SubRelStr of L is full )
thus ( not the non empty full sups-inheriting SubRelStr of L is empty & the non empty full sups-inheriting SubRelStr of L is sups-inheriting & the non empty full sups-inheriting SubRelStr of L is finite-sups-inheriting & the non empty full sups-inheriting SubRelStr of L is bottom-inheriting & the non empty full sups-inheriting SubRelStr of L is full ) ; :: thesis: verum