let R be non empty RelStr ; :: thesis: for f being Function of the carrier of R,(bool the carrier of R)
for x, y being Subset of R holds ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) = (Flip (ff_0 f)) . (x /\ y)

let f be Function of the carrier of R,(bool the carrier of R); :: thesis: for x, y being Subset of R holds ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) = (Flip (ff_0 f)) . (x /\ y)
let x, y be Subset of R; :: thesis: ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) = (Flip (ff_0 f)) . (x /\ y)
AA: (ff_0 f) . ((x /\ y) `) = { u where u is Element of R : f . u meets (x /\ y) ` } by Defff;
AB: (ff_0 f) . (x `) = { u where u is Element of R : f . u meets x ` } by Defff;
AC: (ff_0 f) . (y `) = { u where u is Element of R : f . u meets y ` } by Defff;
thus ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) c= (Flip (ff_0 f)) . (x /\ y) :: according to XBOOLE_0:def 10 :: thesis: (Flip (ff_0 f)) . (x /\ y) c= ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) or t in (Flip (ff_0 f)) . (x /\ y) )
assume zz: t in ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) ; :: thesis: t in (Flip (ff_0 f)) . (x /\ y)
then ZZ: ( t in (Flip (ff_0 f)) . x & t in (Flip (ff_0 f)) . y ) by XBOOLE_0:def 4;
then t in ((ff_0 f) . (x `)) ` by ROUGHS_2:def 14;
then Z1: not t in (ff_0 f) . (x `) by XBOOLE_0:def 5;
t in ((ff_0 f) . (y `)) ` by ;
then V1: not t in (ff_0 f) . (y `) by XBOOLE_0:def 5;
not t in (ff_0 f) . ((x /\ y) `)
proof
assume t in (ff_0 f) . ((x /\ y) `) ; :: thesis: contradiction
then consider w being Element of R such that
A1: ( t = w & f . w meets (x /\ y) ` ) by AA;
f . w meets (x `) \/ (y `) by ;
end;
then t in ((ff_0 f) . ((x /\ y) `)) ` by ;
hence t in (Flip (ff_0 f)) . (x /\ y) by ROUGHS_2:def 14; :: thesis: verum
end;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (Flip (ff_0 f)) . (x /\ y) or t in ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) )
assume v0: t in (Flip (ff_0 f)) . (x /\ y) ; :: thesis: t in ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y)
then t in ((ff_0 f) . ((x /\ y) `)) ` by ROUGHS_2:def 14;
then ww: not t in { u where u is Element of R : f . u meets (x /\ y) ` } by ;
vc: (x /\ y) ` = (x `) \/ (y `) by XBOOLE_1:54;
w1: not t in (ff_0 f) . (x `)
proof
assume t in (ff_0 f) . (x `) ; :: thesis: contradiction
then consider w being Element of R such that
A1: ( t = w & f . w meets x ` ) by AB;
f . w meets (x /\ y) ` by ;
hence contradiction by ww, A1; :: thesis: verum
end;
z1: not t in (ff_0 f) . (y `)
proof
assume t in (ff_0 f) . (y `) ; :: thesis: contradiction
then consider w being Element of R such that
A1: ( t = w & f . w meets y ` ) by AC;
f . w meets (x /\ y) ` by ;
hence contradiction by ww, A1; :: thesis: verum
end;
t in ((ff_0 f) . (x `)) ` by ;
then W1: t in (Flip (ff_0 f)) . x by ROUGHS_2:def 14;
t in ((ff_0 f) . (y `)) ` by ;
then t in (Flip (ff_0 f)) . y by ROUGHS_2:def 14;
hence t in ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) by ; :: thesis: verum