let R be non empty RelStr ; :: thesis: ( R is reflexive implies Flip (f_1 R) cc= id (bool the carrier of R) )
assume TT: R is reflexive ; :: thesis: Flip (f_1 R) cc= id (bool the carrier of R)
set f = Flip (f_1 R);
set g = id (bool the carrier of R);
A1: dom (Flip (f_1 R)) c= dom (id (bool the carrier of R)) ;
for i being set st i in dom (Flip (f_1 R)) holds
(Flip (f_1 R)) . i c= (id (bool the carrier of R)) . i

proof

let i be set ; :: thesis: ( i in dom (Flip (f_1 R)) implies (Flip (f_1 R)) . i c= (id (bool the carrier of R)) . i )
assume i in dom (Flip (f_1 R)) ; :: thesis: (Flip (f_1 R)) . i c= (id (bool the carrier of R)) . i
then reconsider ii = i as Subset of R ;
{ w where w is Element of R : (UncertaintyMap R) . w c= ii } c= ii

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in { w where w is Element of R : (UncertaintyMap R) . w c= ii } or r in ii )
assume r in { w where w is Element of R : (UncertaintyMap R) . w c= ii } ; :: thesis: r in ii
then consider w being Element of R such that
C4: ( r = w & (UncertaintyMap R) . w c= ii ) ;
thus r in ii by C4, TT, ReflUnc; :: thesis: verum

end;

hence (Flip (f_1 R)) . i c= (id (bool the carrier of R)) . i by FlipF1; :: thesis: verum

end;

hence Flip (f_1 R) cc= id (bool the carrier of R) by A1, ALTCAT_2:def 1; :: thesis: verum