theorem Th5: :: WAYBEL23:5

for L being complete sup-Semilattice
for S being non empty full join-inheriting SubRelStr of L st Bottom L in the carrier of S holds
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups Y c= finsups X