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
proof
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;
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 )
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
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 yy in ((f_0 R) . (x `)) ` by XBOOLE_0:def 5;
hence y in (Flip (f_0 R)) . x by ROUGHS_2:def 14; :: thesis: verum