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

proof

let x, y be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: 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 A1, Th49; :: thesis: verum

end;

let x, y be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for b₁ being object 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 object 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 A1, Th50; :: thesis: verum