let R be Relation; :: thesis: ( R is irreflexive implies R ~ is irreflexive )
assume R is irreflexive ; :: thesis: R ~ is irreflexive
then A1: R is_irreflexive_in field R by Def10;

now

let x be set ; :: 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, Def2;
hence not [x,x] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

then R ~ is_irreflexive_in field (R ~) by Def2;
hence R ~ is irreflexive by Def10; :: thesis: verum