theorem :: WAYBEL21:17

for T being lower-bounded sup-Semilattice
for S being non empty full join-inheriting SubRelStr of T st Bottom T in the carrier of S & S is directed-sups-inheriting holds
S is sups-inheriting