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 reflexive & W is connected ) by A3, WELLORD1:def 4;
then A4: ( W is_reflexive_in field W & W is_connected_in field W ) by RELAT_2:def 9, RELAT_2:def 14;
then A5: ( not x <> y or [x,y] in W or [y,x] in W ) by A1, A2, RELAT_2:def 6;
assume not x in W -Seg y ; :: thesis: [y,x] in W
hence [y,x] in W by A1, A4, A5, RELAT_2:def 1, WELLORD1:def 1; :: thesis: verum