let a, b be object ; :: thesis: ( a <> b implies {[a,b]} is asymmetric )
assume A0: a <> b ; :: thesis: {[a,b]} is asymmetric
set R = {[a,b]};
for x, y being object st [x,y] in {[a,b]} holds
not [y,x] in {[a,b]}

proof

let x, y be object ; :: thesis: ( [x,y] in {[a,b]} implies not [y,x] in {[a,b]} )
assume [x,y] in {[a,b]} ; :: thesis: not [y,x] in {[a,b]}
then [x,y] = [a,b] by TARSKI:def 1;
then A1: ( x = a & y = b ) by XTUPLE_0:1;
assume [y,x] in {[a,b]} ; :: thesis: contradiction
then [y,x] = [a,b] by TARSKI:def 1;
hence contradiction by A0, A1, XTUPLE_0:1; :: thesis: verum

end;

hence {[a,b]} is asymmetric by LemAsym; :: thesis: verum