let z be Complex; :: thesis: for X being complex-membered set st z <> 1 & z <> - 1 & not 0 in X holds
multRel (X,z) is asymmetric
let X be complex-membered set ; :: thesis: ( z <> 1 & z <> - 1 & not 0 in X implies multRel (X,z) is asymmetric )
assume A0: ( z <> 1 & z <> - 1 & not 0 in X ) ; :: thesis: multRel (X,z) is asymmetric

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

let x, y be object ; :: thesis: ( x in field (multRel (X,z)) & y in field (multRel (X,z)) & [x,y] in multRel (X,z) implies not [y,x] in multRel (X,z) )
reconsider a = x, b = y as set by TARSKI:1;
assume A1: ( x in field (multRel (X,z)) & y in field (multRel (X,z)) & [x,y] in multRel (X,z) & [y,x] in multRel (X,z) ) ; :: thesis: contradiction
then A2: ( 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, Th42;
then b = z * (z * b) ;
then b * (b ") = ((z * z) * b) * (b ")
.= (z * z) * (b * (b ")) ;
then 1 = (z * z) * (b * (b ")) by A0, A2, XCMPLX_0:def 7;
then 1 = (z * z) * 1 by A0, A2, XCMPLX_0:def 7;
hence contradiction by A0, XCMPLX_1:182; :: thesis: verum

end;

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