let R be Relation; :: thesis: ( R is reflexive iff for x being set st x in field R holds
[x,x] in R )
( R is reflexive iff R is_reflexive_in field R ) by RELAT_2:def 9;
hence ( R is reflexive iff for x being set st x in field R holds
[x,x] in R ) by RELAT_2:def 1; :: thesis: verum