theorem Th8: :: WAYBEL12:8

for L being non empty antisymmetric upper-bounded RelStr
for X being non empty upper Subset of L holds Top L in X