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