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 & y in field W ) and
A2: W is well-ordering ; :: thesis: ( not x in W -Seg y or not [y,x] in W )
W is antisymmetric by A2;
then A3: W is_antisymmetric_in field W by RELAT_2:def 12;
assume x in W -Seg y ; :: thesis: not [y,x] in W
then A4: ( x <> y & [x,y] in W ) by WELLORD1:1;
assume [y,x] in W ; :: thesis: contradiction
hence contradiction by A1, A3, A4, RELAT_2:def 4; :: thesis: verum