let R be Relation; :: thesis: for x being set st x is_maximal_in R & R is connected holds
x is_superior_of R
let x be set ; :: thesis: ( x is_maximal_in R & R is connected implies x is_superior_of R )
assume that
A1: x is_maximal_in R and
A2: R is connected ; :: thesis: x is_superior_of R
thus A3: x in field R by A1, Def11; :: according to ORDERS_1:def 13 :: thesis: for y being set st y in field R & y <> x holds
[y,x] in R
let y be set ; :: thesis: ( y in field R & y <> x implies [y,x] in R )
assume that
A4: y in field R and
A5: y <> x ; :: thesis: [y,x] in R
R is_connected_in field R by A2, RELAT_2:def 14;
then ( [x,y] in R or [y,x] in R ) by A3, A4, A5, RELAT_2:def 6;
hence [y,x] in R by A1, A4, Def11; :: thesis: verum