let a, b be set ; :: thesis: ( R2(a,b) implies not R2(b,a) )
assume A1: ( a in b & b in a ) ; :: thesis: contradiction
set X = {a,b};
A3: ( a in {a,b} & b in {a,b} ) by Def2;
consider Y being set such that
A4: ( Y in {a,b} & ( for x being object holds
( not x in {a,b} or not x in Y ) ) ) by A3, TARSKI_0:5;
( Y = a or Y = b ) by A4, Def2;
hence contradiction by A1, A3, A4; :: thesis: verum