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