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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Flip (ff_0 f)) . x or y in { w where w is Element of R : f . w c= x } )
assume S1: y in (Flip (ff_0 f)) . x ; :: thesis: y in { w where w is Element of R : f . w c= x }
then y in ((ff_0 f) . (x `)) ` by ROUGHS_2:def 14;
then Z1: not y in (ff_0 f) . (x `) by XBOOLE_0:def 5;
reconsider yy = y as Element of R by S1;
f . yy misses x ` by Z1, ZZ;
then f . yy c= x by SUBSET_1:24;
hence y in { w where w is Element of R : f . 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 : f . w c= x } or y in (Flip (ff_0 f)) . x )
assume y in { w where w is Element of R : f . w c= x } ; :: thesis: y in (Flip (ff_0 f)) . x
then consider w being Element of R such that
L1: ( y = w & f . w c= x ) ;
reconsider yy = y as Element of R by L1;
not yy in (ff_0 f) . (x `)

proof

assume yy in (ff_0 f) . (x `) ; :: thesis: contradiction
then consider v being Element of R such that
L2: ( yy = v & f . v meets x ` ) by ZZ;
thus contradiction by L1, L2, SUBSET_1:24; :: thesis: verum

end;

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