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) c= (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) c= (Flip (ff_0 f)) . (x \/ y)

let x, y be Subset of R; :: thesis: ((Flip (ff_0 f)) . x) \/ ((Flip (ff_0 f)) . y) c= (Flip (ff_0 f)) . (x \/ y)

AA: (Flip (ff_0 f)) . (x \/ y) = { u where u is Element of R : f . u c= x \/ y } by FlipFF;

AB: (Flip (ff_0 f)) . x = { u where u is Element of R : f . u c= x } by FlipFF;

AC: (Flip (ff_0 f)) . y = { u where u is Element of R : f . u c= y } by FlipFF;

XX: ( x c= x \/ y & y c= x \/ y ) by XBOOLE_1:7;

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

for x, y being Subset of R holds ((Flip (ff_0 f)) . x) \/ ((Flip (ff_0 f)) . y) c= (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) c= (Flip (ff_0 f)) . (x \/ y)

let x, y be Subset of R; :: thesis: ((Flip (ff_0 f)) . x) \/ ((Flip (ff_0 f)) . y) c= (Flip (ff_0 f)) . (x \/ y)

AA: (Flip (ff_0 f)) . (x \/ y) = { u where u is Element of R : f . u c= x \/ y } by FlipFF;

AB: (Flip (ff_0 f)) . x = { u where u is Element of R : f . u c= x } by FlipFF;

AC: (Flip (ff_0 f)) . y = { u where u is Element of R : f . u c= y } by FlipFF;

XX: ( x c= x \/ y & y c= x \/ y ) by XBOOLE_1:7;

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

per cases then
( t in (Flip (ff_0 f)) . x or t in (Flip (ff_0 f)) . y )
by XBOOLE_0:def 3;

end;