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 object st x in X holds

ex y being object st [y,x] in R

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 object st x in X holds

ex y being object st [y,x] in R

proof

hence
rng R = X
by RELSET_1:10; :: thesis: verum
let x be object ; :: thesis: ( x in X implies ex y being object st [y,x] in R )

assume A2: x in X ; :: thesis: ex y being object st [y,x] in R

take x ; :: thesis: [x,x] in R

thus [x,x] in R by A1, A2, RELAT_2:def 1; :: thesis: verum

end;assume A2: x in X ; :: thesis: ex y being object st [y,x] in R

take x ; :: thesis: [x,x] in R

thus [x,x] in R by A1, A2, RELAT_2:def 1; :: thesis: verum