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 ZZ, ROUGHS_2:def 14;
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 XBOOLE_1:54, A1;

per cases then ( f . w meets x ` or f . w meets y ` ) by XBOOLE_1:70;

suppose f . w meets x ` ; :: thesis: contradiction

hence contradiction by Z1, A1, AB; :: thesis: verum

end;

suppose f . w meets y ` ; :: thesis: contradiction

hence contradiction by V1, AC, A1; :: thesis: verum

end;

end;

end;

then t in ((ff_0 f) . ((x /\ y) `)) ` by zz, XBOOLE_0:def 5;
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 AA, XBOOLE_0:def 5;
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 vc, A1, XBOOLE_1:63, XBOOLE_1:7;
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 vc, A1, XBOOLE_1:63, XBOOLE_1:7;
hence contradiction by ww, A1; :: thesis: verum

end;

t in ((ff_0 f) . (x `)) ` by w1, v0, XBOOLE_0:def 5;
then W1: t in (Flip (ff_0 f)) . x by ROUGHS_2:def 14;
t in ((ff_0 f) . (y `)) ` by z1, v0, XBOOLE_0:def 5;
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 W1, XBOOLE_0:def 4; :: thesis: verum