A1: R is_reflexive_in field R by Def9;
let x be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( x in field (R ~) implies [x,x] in R ~ )
assume x in field (R ~) ; :: thesis: [x,x] in R ~
then x in field R by RELAT_1:21;
then [x,x] in R by A1;
hence [x,x] in R ~ by RELAT_1:def 7; :: thesis: verum