let R be non empty RelStr ; :: thesis: ( R is reflexive implies union (() .: ([#] R)) = the carrier of R )
assume AA: R is reflexive ; :: thesis: union (() .: ([#] R)) = the carrier of R
B1: the carrier of R c= union (() .: ([#] R))
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in the carrier of R or t in union (() .: ([#] R)) )
assume t in the carrier of R ; :: thesis: t in union (() .: ([#] R))
then reconsider tt = t as Element of R ;
dom () = the carrier of R by FUNCT_2:def 1;
then A2: ( tt in dom () & tt in [#] R ) ;
A3: tt in () . t by ;
(UncertaintyMap R) . t in () .: ([#] R) by ;
hence t in union (() .: ([#] R)) by ; :: thesis: verum
end;
union (() .: ([#] R)) c= the carrier of R
proof
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in union (() .: ([#] R)) or f in the carrier of R )
assume f in union (() .: ([#] R)) ; :: thesis: f in the carrier of R
then ex tt being set st
( f in tt & tt in () .: ([#] R) ) by TARSKI:def 4;
hence f in the carrier of R ; :: thesis: verum
end;
hence union (() .: ([#] R)) = the carrier of R by B1; :: thesis: verum