let S be SubRelStr of L; :: thesis: ( S is sups-inheriting implies not S is empty )

assume A2: S is sups-inheriting ; :: thesis: not S is empty

ex_sup_of {} S,L by YELLOW_0:17;

hence not S is empty by A2; :: thesis: verum

assume A2: S is sups-inheriting ; :: thesis: not S is empty

ex_sup_of {} S,L by YELLOW_0:17;

hence not S is empty by A2; :: thesis: verum