let R be non empty RelStr ; :: thesis: ( R is reflexive implies union ((UncertaintyMap R) .: ([#] R)) = the carrier of R )
assume AA: R is reflexive ; :: thesis: union ((UncertaintyMap R) .: ([#] R)) = the carrier of R
B1: the carrier of R c= union ((UncertaintyMap R) .: ([#] R))

proof

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

end;

union ((UncertaintyMap R) .: ([#] R)) c= the carrier of R

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in union ((UncertaintyMap R) .: ([#] R)) or f in the carrier of R )
assume f in union ((UncertaintyMap R) .: ([#] R)) ; :: thesis: f in the carrier of R
then ex tt being set st
( f in tt & tt in (UncertaintyMap R) .: ([#] R) ) by TARSKI:def 4;
hence f in the carrier of R ; :: thesis: verum

end;

hence union ((UncertaintyMap R) .: ([#] R)) = the carrier of R by B1; :: thesis: verum