let R be non empty RelStr ; :: thesis: for I being Function of the carrier of R,(bool the carrier of R) st I is map-reflexive holds
the carrier of R = union (I .: ([#] R))
let I be Function of the carrier of R,(bool the carrier of R); :: thesis: ( I is map-reflexive implies the carrier of R = union (I .: ([#] R)) )
assume AA: I is map-reflexive ; :: thesis: the carrier of R = union (I .: ([#] R))
thus the carrier of R c= union (I .: ([#] R)) :: according to XBOOLE_0:def 10 :: thesis: union (I .: ([#] R)) c= the carrier of R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in union (I .: ([#] R)) )
assume A0: x in the carrier of R ; :: thesis: x in union (I .: ([#] R))
then reconsider y = x as Element of R ;
A2: y in I . x by AA;
x in dom I by A0, FUNCT_2:def 1;
then I . x in I .: ([#] R) by FUNCT_1:def 6;
hence x in union (I .: ([#] R)) by A2, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (I .: ([#] R)) or x in the carrier of R )
assume x in union (I .: ([#] R)) ; :: thesis: x in the carrier of R
then consider y being set such that
T1: ( x in y & y in I .: ([#] R) ) by TARSKI:def 4;
thus x in the carrier of R by T1; :: thesis: verum