let x, y be set ; :: thesis: for W being Relation st x in field W & y in field W & W is well-ordering & not x in W -Seg y holds
[y,x] in W
let W be Relation; :: thesis: ( x in field W & y in field W & W is well-ordering & not x in W -Seg y implies [y,x] in W )
assume that
A1: x in field W and
A2: y in field W and
A3: W is well-ordering ; :: thesis: ( x in W -Seg y or [y,x] in W )
W is connected by A3;
then W is_connected_in field W by RELAT_2:def 14;
then A4: ( not x <> y or [x,y] in W or [y,x] in W ) by A1, A2, RELAT_2:def 6;
W is reflexive by A3;
then A5: W is_reflexive_in field W by RELAT_2:def 9;
assume not x in W -Seg y ; :: thesis: [y,x] in W
hence [y,x] in W by A1, A5, A4, RELAT_2:def 1, WELLORD1:1; :: thesis: verum