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;
then "\/" ({} S),L in the carrier of S by A2, YELLOW_0:def 19;
hence not S is empty ; :: thesis: verum