let A be set ; :: thesis: for R being Relation of A st R is_reflexive_in A holds
( dom R = A & field R = A )
let R be Relation of A; :: thesis: ( R is_reflexive_in A implies ( dom R = A & field R = A ) )
assume A1: R is_reflexive_in A ; :: thesis: ( dom R = A & field R = A )
A2: A c= dom R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in dom R )
assume x in A ; :: thesis: x in dom R
then [x,x] in R by A1, RELAT_2:def 1;
hence x in dom R by RELAT_1:def 4; :: thesis: verum

end;

hence dom R = A by XBOOLE_0:def 10; :: thesis: field R = A
thus field R = A \/ (rng R) by A2, XBOOLE_0:def 10
.= A by XBOOLE_1:12 ; :: thesis: verum