theorem :: ORDERS_1:56
for R being Relation
for x being set st x is_maximal_in R & R is connected holds
x is_superior_of R