let R be non empty RelStr ; :: thesis: ( the InternalRel of R is total & the InternalRel of R is reflexive implies id (bool the carrier of R) cc= f_0 R )

assume zz: ( the InternalRel of R is total & the InternalRel of R is reflexive ) ; :: thesis: id (bool the carrier of R) cc= f_0 R

set f = id (bool the carrier of R);

set g = f_0 R;

A1: dom (id (bool the carrier of R)) c= dom (f_0 R) by FUNCT_2:def 1;

for i being set st i in dom (id (bool the carrier of R)) holds

(id (bool the carrier of R)) . i c= (f_0 R) . i

assume zz: ( the InternalRel of R is total & the InternalRel of R is reflexive ) ; :: thesis: id (bool the carrier of R) cc= f_0 R

set f = id (bool the carrier of R);

set g = f_0 R;

A1: dom (id (bool the carrier of R)) c= dom (f_0 R) by FUNCT_2:def 1;

for i being set st i in dom (id (bool the carrier of R)) holds

(id (bool the carrier of R)) . i c= (f_0 R) . i

proof

hence
id (bool the carrier of R) cc= f_0 R
by A1, ALTCAT_2:def 1; :: thesis: verum
let i be set ; :: thesis: ( i in dom (id (bool the carrier of R)) implies (id (bool the carrier of R)) . i c= (f_0 R) . i )

assume k2: i in dom (id (bool the carrier of R)) ; :: thesis: (id (bool the carrier of R)) . i c= (f_0 R) . i

then reconsider ii = i as Subset of R ;

i c= { u where u is Element of R : (tau R) . u meets ii }

end;assume k2: i in dom (id (bool the carrier of R)) ; :: thesis: (id (bool the carrier of R)) . i c= (f_0 R) . i

then reconsider ii = i as Subset of R ;

i c= { u where u is Element of R : (tau R) . u meets ii }

proof

hence
(id (bool the carrier of R)) . i c= (f_0 R) . i
by Defff; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in i or y in { u where u is Element of R : (tau R) . u meets ii } )

assume D1: y in i ; :: thesis: y in { u where u is Element of R : (tau R) . u meets ii }

then reconsider wy = y as Element of R by k2;

[wy,wy] in the InternalRel of R by zz, LATTAD_1:1;

then wy in (tau R) . wy by For3A;

then (tau R) . wy meets ii by XBOOLE_0:3, D1;

hence y in { u where u is Element of R : (tau R) . u meets ii } ; :: thesis: verum

end;assume D1: y in i ; :: thesis: y in { u where u is Element of R : (tau R) . u meets ii }

then reconsider wy = y as Element of R by k2;

[wy,wy] in the InternalRel of R by zz, LATTAD_1:1;

then wy in (tau R) . wy by For3A;

then (tau R) . wy meets ii by XBOOLE_0:3, D1;

hence y in { u where u is Element of R : (tau R) . u meets ii } ; :: thesis: verum