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

let x, y be object ; :: thesis: ( x in field (addRel (X,z)) & y in field (addRel (X,z)) & [x,y] in addRel (X,z) implies not [y,x] in addRel (X,z) )
reconsider a = x, b = y as set by TARSKI:1;
assume A1: ( x in field (addRel (X,z)) & y in field (addRel (X,z)) & [x,y] in addRel (X,z) & [y,x] in addRel (X,z) ) ; :: thesis: contradiction
then ( a in X & b in X ) by MMLQUER2:4;
then reconsider a = a, b = b as Complex ;
( b = z + a & a = z + b ) by A1, Th11;
then 0 = 2 * z ;
hence contradiction ; :: thesis: verum

end;

hence addRel (X,z) is asymmetric by RELAT_2:def 13, RELAT_2:def 5; :: thesis: verum