let R be non empty RelStr ; :: thesis: for x being Subset of R holds (Flip (f_1 R)) . x = { w where w is Element of R : (UncertaintyMap R) . w c= x }
let x be Subset of R; :: thesis: (Flip (f_1 R)) . x = { w where w is Element of R : (UncertaintyMap R) . w c= x }
ZZ: (f_1 R) . (x `) = { w where w is Element of R : (UncertaintyMap R) . w meets x ` } by Defff;
thus (Flip (f_1 R)) . x c= { w where w is Element of R : (UncertaintyMap R) . w c= x } :: according to XBOOLE_0:def 10 :: thesis: { w where w is Element of R : (UncertaintyMap R) . w c= x } c= (Flip (f_1 R)) . x

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Flip (f_1 R)) . x or y in { w where w is Element of R : (UncertaintyMap R) . w c= x } )
assume S1: y in (Flip (f_1 R)) . x ; :: thesis: y in { w where w is Element of R : (UncertaintyMap R) . w c= x }
then y in ((f_1 R) . (x `)) ` by ROUGHS_2:def 14;
then Z1: not y in (f_1 R) . (x `) by XBOOLE_0:def 5;
reconsider yy = y as Element of R by S1;
(UncertaintyMap R) . yy misses x ` by Z1, ZZ;
then (UncertaintyMap R) . yy c= x by SUBSET_1:24;
hence y in { w where w is Element of R : (UncertaintyMap R) . w c= x } ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { w where w is Element of R : (UncertaintyMap R) . w c= x } or y in (Flip (f_1 R)) . x )
assume y in { w where w is Element of R : (UncertaintyMap R) . w c= x } ; :: thesis: y in (Flip (f_1 R)) . x
then consider w being Element of R such that
L1: ( y = w & (UncertaintyMap R) . w c= x ) ;
reconsider yy = y as Element of R by L1;
not yy in (f_1 R) . (x `)

proof

assume yy in (f_1 R) . (x `) ; :: thesis: contradiction
then ex v being Element of R st
( yy = v & (UncertaintyMap R) . v meets x ` ) by ZZ;
hence contradiction by L1, SUBSET_1:24; :: thesis: verum

end;

then yy in ((f_1 R) . (x `)) ` by XBOOLE_0:def 5;
hence y in (Flip (f_1 R)) . x by ROUGHS_2:def 14; :: thesis: verum