let R be non empty RelStr ; :: thesis: ( the InternalRel of R is reflexive & the InternalRel of R is total implies (f_1 R) . the carrier of R = the carrier of R )
assume RR: ( the InternalRel of R is reflexive & the InternalRel of R is total ) ; :: thesis: (f_1 R) . the carrier of R = the carrier of R
A0: (f_1 R) . ([#] R) = { u where u is Element of R : (UncertaintyMap R) . u meets [#] R } by Defff;
the carrier of R c= { u where u is Element of R : (UncertaintyMap R) . u meets [#] R }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of R or y in { u where u is Element of R : (UncertaintyMap R) . u meets [#] R } )
assume y in the carrier of R ; :: thesis: y in { u where u is Element of R : (UncertaintyMap R) . u meets [#] R }
then reconsider u = y as Element of R ;
[u,u] in the InternalRel of R by LATTAD_1:1, RR;
then u in (UncertaintyMap R) . u by For3;
then consider u being Element of R such that
A1: ( u = y & (UncertaintyMap R) . u meets [#] R ) by XBOOLE_0:3;
thus y in { u where u is Element of R : (UncertaintyMap R) . u meets [#] R } by A1; :: thesis: verum

end;

hence (f_1 R) . the carrier of R = the carrier of R by A0; :: thesis: verum