set N = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ;
inversions R = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) }

proof

thus inversions R c= { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } :: according to XBOOLE_0:def 10 :: thesis: { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } c= inversions R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in inversions R or x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } )
assume x in inversions R ; :: thesis: x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) }
then consider a, b being Element of dom R such that
A1: ( x = [a,b] & a in b & not R /. a <= R /. b ) ;
R /. a > R /. b by A1, Th45;
hence x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } or x in inversions R )
assume x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ; :: thesis: x in inversions R
then consider a, b being Element of dom R such that
A2: ( x = [a,b] & a in b & R /. a > R /. b ) ;
not R /. a <= R /. b by A2, Th45;
hence x in inversions R by A2; :: thesis: verum

end;

hence for b₁ being set holds
( b₁ = inversions R iff b₁ = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ) ; :: thesis: verum