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

hereby :: thesis: ( id (field R) c= R implies R is reflexive )

assume A1: R is reflexive ; :: thesis: id (field R) c= R
thus id (field R) c= R :: thesis: verum

proof

let a, b be object ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in id (field R) or [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 A1, Def1; :: thesis: verum

end;

end;

assume A2: id (field R) c= R ; :: thesis: R is reflexive
let a be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: 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