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 implies R is_reflexive_in field R ) & ( R is_reflexive_in field R implies R is reflexive ) & ( R is_reflexive_in field R implies for x being set st x in field R holds
[x,x] in R ) & ( ( for x being set st x in field R holds
[x,x] in R ) implies R is_reflexive_in field R ) ) by RELAT_2:def 1, RELAT_2:def 9;
hence ( R is reflexive iff for x being set st x in field R holds
[x,x] in R ) ; :: thesis: verum