let R be Relation; :: thesis: ( R is reflexive iff id (field R) c= R )

A1: now

assume A2: id (field R) c= R ; :: thesis: R is reflexive

now

let a be set ; :: thesis: ( a in field R implies [a,a] in R )
assume a in field R ; :: thesis: [a,a] in R
then [a,a] in id (field R) by RELAT_1:def 10;
hence [a,a] in R by A2; :: thesis: verum

end;

then R is_reflexive_in field R by Def1;
hence R is reflexive by Def9; :: thesis: verum

end;

now

assume R is reflexive ; :: thesis: id (field R) c= R
then A3: R is_reflexive_in field R by Def9;

now

let a, b be set ; :: thesis: ( [a,b] in id (field R) implies [a,b] in R )
assume [a,b] in id (field R) ; :: thesis: [a,b] in R
then ( a in field R & a = b ) by RELAT_1:def 10;
hence [a,b] in R by A3, Def1; :: thesis: verum

end;

hence id (field R) c= R by RELAT_1:def 3; :: thesis: verum

end;

hence ( R is reflexive iff id (field R) c= R ) by A1; :: thesis: verum