theorem Th3: :: WAYBEL23:3

for L being non empty transitive RelStr
for S being non empty full sups-inheriting SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X c= finsups Y