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

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 `)

hence y in (Flip (ff_0 f)) . x by ROUGHS_2:def 14; :: thesis: verum

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 { w where w is Element of R : f . w c= x } or y in (Flip (ff_0 f)) . x )
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;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

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

then
yy in ((ff_0 f) . (x `)) `
by XBOOLE_0:def 5;
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 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

hence y in (Flip (ff_0 f)) . x by ROUGHS_2:def 14; :: thesis: verum