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