theorem Th14: :: WAYBEL20:14

for L being non empty antisymmetric RelStr
for X being Subset of [:L,L:] st X c= id the carrier of L & ex_sup_of X,[:L,L:] holds
sup X in id the carrier of L