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)

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

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

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 /\ y) or t in ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) )
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) `)

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

end;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

then
t in ((ff_0 f) . ((x /\ y) `)) `
by zz, XBOOLE_0:def 5;
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;

end;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;

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

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

z1:
not t in (ff_0 f) . (y `)
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;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

proof

t in ((ff_0 f) . (x `)) `
by w1, v0, XBOOLE_0:def 5;
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;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

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