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 (ff_0 f) . (x \/ y) = ((ff_0 f) . x) \/ ((ff_0 f) . y)
let f be Function of the carrier of R,(bool the carrier of R); :: thesis: for x, y being Subset of R holds (ff_0 f) . (x \/ y) = ((ff_0 f) . x) \/ ((ff_0 f) . y)
let x, y be Subset of R; :: thesis: (ff_0 f) . (x \/ y) = ((ff_0 f) . x) \/ ((ff_0 f) . 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 (ff_0 f) . (x \/ y) c= ((ff_0 f) . x) \/ ((ff_0 f) . y) :: according to XBOOLE_0:def 10 :: thesis: ((ff_0 f) . x) \/ ((ff_0 f) . y) c= (ff_0 f) . (x \/ y)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (ff_0 f) . (x \/ y) or t in ((ff_0 f) . x) \/ ((ff_0 f) . y) )
assume t in (ff_0 f) . (x \/ y) ; :: thesis: t in ((ff_0 f) . x) \/ ((ff_0 f) . y)
then consider u being Element of R such that
A1: ( t = u & f . u meets x \/ y ) by AA;
( f . u meets x or f . u meets y ) by A1, XBOOLE_1:70;
then ( t in (ff_0 f) . x or t in (ff_0 f) . y ) by A1, AB, AC;
hence t in ((ff_0 f) . x) \/ ((ff_0 f) . y) by XBOOLE_0:def 3; :: thesis: verum

end;

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in ((ff_0 f) . x) \/ ((ff_0 f) . y) or t in (ff_0 f) . (x \/ y) )
assume t in ((ff_0 f) . x) \/ ((ff_0 f) . y) ; :: thesis: t in (ff_0 f) . (x \/ y)

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

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

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

end;

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

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

end;

end;