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 }

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

hence
(f_0 R) . the carrier of R = the carrier of R
by A0; :: thesis: verum
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;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