let r be Relation; :: thesis: ( r = inversions R implies ( r is asymmetric & r is transitive ) )
assume Z0: r = inversions R ; :: thesis: ( r is asymmetric & r is transitive )
thus r is asymmetric :: thesis: r is transitive

proof

let x be set ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: for b₁ being set holds
( not x in field r or not b₁ in field r or not [x,b₁] in r or not [b₁,x] in r )
let y be set ; :: thesis: ( not x in field r or not y in field r or not [x,y] in r or not [y,x] in r )
thus ( not x in field r or not y in field r or not [x,y] in r or not [y,x] in r ) by Z0, TW2; :: thesis: verum

end;

let x be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for b₁, b₂ being set holds
( not x in field r or not b₁ in field r or not b₂ in field r or not [x,b₁] in r or not [b₁,b₂] in r or [x,b₂] in r )
let y be set ; :: thesis: for b₁ being set holds
( not x in field r or not y in field r or not b₁ in field r or not [x,y] in r or not [y,b₁] in r or [x,b₁] in r )
thus for b₁ being set holds
( not x in field r or not y in field r or not b₁ in field r or not [x,y] in r or not [y,b₁] in r or [x,b₁] in r ) by Z0, TW3; :: thesis: verum