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)

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

suppose t in (Flip (ff_0 f)) . x ; :: thesis: t in (Flip (ff_0 f)) . (x \/ y)

then consider u being Element of R such that
A1: ( t = u & f . u c= x ) by AB;
f . u c= x \/ y by A1, XX;
hence t in (Flip (ff_0 f)) . (x \/ y) by A1, AA; :: thesis: verum

end;

suppose t in (Flip (ff_0 f)) . y ; :: thesis: t in (Flip (ff_0 f)) . (x \/ y)

then consider u being Element of R such that
A1: ( t = u & f . u c= y ) by AC;
f . u c= x \/ y by A1, XX;
hence t in (Flip (ff_0 f)) . (x \/ y) by A1, AA; :: thesis: verum

end;

end;