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) c= ((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) c= ((ff_0 f) . x) /\ ((ff_0 f) . y)
let x, y be Subset of R; :: thesis: (ff_0 f) . (x /\ y) c= ((ff_0 f) . x) /\ ((ff_0 f) . y)
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;
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 t in { u where u is Element of R : f . u meets x /\ y } by Defff;
then consider u being Element of R such that
A1: ( t = u & f . u meets x /\ y ) ;
( f . u meets x & f . u meets y ) by A1, XBOOLE_1:74;
then ( t in (ff_0 f) . x & 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 4; :: thesis: verum