A1:
R is_irreflexive_in field R
by Def10;

let x be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( x in field (R ~) implies not [x,x] in R ~ )

assume x in field (R ~) ; :: thesis: not [x,x] in R ~

then x in field R by RELAT_1:21;

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

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

let x be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( x in field (R ~) implies not [x,x] in R ~ )

assume x in field (R ~) ; :: thesis: not [x,x] in R ~

then x in field R by RELAT_1:21;

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

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