let R be non empty RelStr ; :: thesis: for x being Subset of R holds (Flip (f_0 R)) . x = { w where w is Element of R : (tau R) . w c= x }

let x be Subset of R; :: thesis: (Flip (f_0 R)) . x = { w where w is Element of R : (tau R) . w c= x }

ZZ: (f_0 R) . (x `) = { w where w is Element of R : (tau R) . w meets x ` } by Defff;

thus (Flip (f_0 R)) . x c= { w where w is Element of R : (tau R) . w c= x } :: according to XBOOLE_0:def 10 :: thesis: { w where w is Element of R : (tau R) . w c= x } c= (Flip (f_0 R)) . x

assume y in { w where w is Element of R : (tau R) . w c= x } ; :: thesis: y in (Flip (f_0 R)) . x

then consider w being Element of R such that

L1: ( y = w & (tau R) . w c= x ) ;

reconsider yy = y as Element of R by L1;

not yy in (f_0 R) . (x `)

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

let x be Subset of R; :: thesis: (Flip (f_0 R)) . x = { w where w is Element of R : (tau R) . w c= x }

ZZ: (f_0 R) . (x `) = { w where w is Element of R : (tau R) . w meets x ` } by Defff;

thus (Flip (f_0 R)) . x c= { w where w is Element of R : (tau R) . w c= x } :: according to XBOOLE_0:def 10 :: thesis: { w where w is Element of R : (tau R) . w c= x } c= (Flip (f_0 R)) . x

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { w where w is Element of R : (tau R) . w c= x } or y in (Flip (f_0 R)) . x )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Flip (f_0 R)) . x or y in { w where w is Element of R : (tau R) . w c= x } )

assume S1: y in (Flip (f_0 R)) . x ; :: thesis: y in { w where w is Element of R : (tau R) . w c= x }

then y in ((f_0 R) . (x `)) ` by ROUGHS_2:def 14;

then Z1: not y in (f_0 R) . (x `) by XBOOLE_0:def 5;

reconsider yy = y as Element of R by S1;

(tau R) . yy misses x ` by Z1, ZZ;

then (tau R) . yy c= x by SUBSET_1:24;

hence y in { w where w is Element of R : (tau R) . w c= x } ; :: thesis: verum

end;assume S1: y in (Flip (f_0 R)) . x ; :: thesis: y in { w where w is Element of R : (tau R) . w c= x }

then y in ((f_0 R) . (x `)) ` by ROUGHS_2:def 14;

then Z1: not y in (f_0 R) . (x `) by XBOOLE_0:def 5;

reconsider yy = y as Element of R by S1;

(tau R) . yy misses x ` by Z1, ZZ;

then (tau R) . yy c= x by SUBSET_1:24;

hence y in { w where w is Element of R : (tau R) . w c= x } ; :: thesis: verum

assume y in { w where w is Element of R : (tau R) . w c= x } ; :: thesis: y in (Flip (f_0 R)) . x

then consider w being Element of R such that

L1: ( y = w & (tau R) . w c= x ) ;

reconsider yy = y as Element of R by L1;

not yy in (f_0 R) . (x `)

proof

then
yy in ((f_0 R) . (x `)) `
by XBOOLE_0:def 5;
assume
yy in (f_0 R) . (x `)
; :: thesis: contradiction

then ex v being Element of R st

( yy = v & (tau R) . v meets x ` ) by ZZ;

hence contradiction by L1, SUBSET_1:24; :: thesis: verum

end;then ex v being Element of R st

( yy = v & (tau R) . v meets x ` ) by ZZ;

hence contradiction by L1, SUBSET_1:24; :: thesis: verum

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