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

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

hereby :: thesis: ( id (field R) c= R implies R is reflexive )
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