let R be non empty RelStr ; :: thesis: ( the InternalRel of R is reflexive & the InternalRel of R is total implies (f_0 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_0 R) . the carrier of R = the carrier of R
A0: (f_0 R) . ([#] R) = { u where u is Element of R : (tau R) . u meets [#] R } by Defff;
the carrier of R c= { u where u is Element of R : (tau 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 : (tau R) . u meets [#] R } )
assume y in the carrier of R ; :: thesis: y in { u where u is Element of R : (tau R) . u meets [#] R }
then reconsider u = y as Element of R ;
ZZ: (tau R) . u = Im ( the InternalRel of R,u) by DefTau;
[u,u] in the InternalRel of R by LATTAD_1:1, RR;
then u in (tau R) . u by RELAT_1:169, ZZ;
then consider u being Element of R such that
A1: ( u = y & (tau R) . u meets [#] R ) by XBOOLE_0:3;
thus y in { u where u is Element of R : (tau R) . u meets [#] R } by A1; :: thesis: verum

end;

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