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