A1:
R is_asymmetric_in field R
by Def13;

let x be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: for y being object st x in field (R ~) & y in field (R ~) & [x,y] in R ~ holds

not [y,x] in R ~

let y be object ; :: thesis: ( x in field (R ~) & y in field (R ~) & [x,y] in R ~ implies not [y,x] in R ~ )

assume that

A2: ( x in field (R ~) & y in field (R ~) ) and

A3: [x,y] in R ~ ; :: thesis: not [y,x] in R ~

A4: [y,x] in R by A3, RELAT_1:def 7;

( x in field R & y in field R ) by A2, RELAT_1:21;

then not [x,y] in R by A1, A4;

hence not [y,x] in R ~ by RELAT_1:def 7; :: thesis: verum

let x be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: for y being object st x in field (R ~) & y in field (R ~) & [x,y] in R ~ holds

not [y,x] in R ~

let y be object ; :: thesis: ( x in field (R ~) & y in field (R ~) & [x,y] in R ~ implies not [y,x] in R ~ )

assume that

A2: ( x in field (R ~) & y in field (R ~) ) and

A3: [x,y] in R ~ ; :: thesis: not [y,x] in R ~

A4: [y,x] in R by A3, RELAT_1:def 7;

( x in field R & y in field R ) by A2, RELAT_1:21;

then not [x,y] in R by A1, A4;

hence not [y,x] in R ~ by RELAT_1:def 7; :: thesis: verum