theorem :: ORDERS_1:54

for R being Relation
for x being set st x is_superior_of R & R is antisymmetric holds
x is_maximal_in R