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

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

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 union (I .: ([#] R)) or x in the carrier of R )
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;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

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