now :: thesis: for x, y being object st x in field (succRel X) & y in field (succRel X) & [x,y] in succRel X holds
not [y,x] in succRel X

let x, y be object ; :: thesis: ( x in field (succRel X) & y in field (succRel X) & [x,y] in succRel X implies not [y,x] in succRel X )
reconsider a = x, b = y as set by TARSKI:1;
assume ( x in field (succRel X) & y in field (succRel X) & [x,y] in succRel X & [y,x] in succRel X ) ; :: thesis: contradiction
then ( b = succ a & a = succ b ) by Def1;
then succ b in b by ORDINAL1:6;
hence contradiction by ORDINAL1:6; :: thesis: verum

end;

hence succRel X is asymmetric by RELAT_2:def 5, RELAT_2:def 13; :: thesis: verum