let X be set ; :: thesis: for R being Relation of X st R is_reflexive_in X holds
rng R = X
let R be Relation of X; :: thesis: ( R is_reflexive_in X implies rng R = X )
assume A1: R is_reflexive_in X ; :: thesis: rng R = X
for x being set st x in X holds
ex y being set st [y,x] in R

proof

let x be set ; :: thesis: ( x in X implies ex y being set st [y,x] in R )
assume A2: x in X ; :: thesis: ex y being set st [y,x] in R
consider x1 being set such that
A3: x1 = x ;
take x1 ; :: thesis: [x1,x] in R
thus [x1,x] in R by A1, A2, A3, RELAT_2:def 1; :: thesis: verum

end;

hence rng R = X by RELSET_1:10; :: thesis: verum