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 b1 being object holds
( not x in field r or not y in field r or not b1 in field r or not [x,y] in r or not [y,b1] in r or [x,b1] in r )
thus for b1 being object holds
( not x in field r or not y in field r or not b1 in field r or not [x,y] in r or not [y,b1] in r or [x,b1] in r ) by A1, Th50; :: thesis: verum