let P, R be Relation; :: thesis: field (P /\ R) c= (field P) /\ (field R)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in field (P /\ R) or x in (field P) /\ (field R) )
assume x in field (P /\ R) ; :: thesis: x in (field P) /\ (field R)
then A1: ( x in dom (P /\ R) or x in rng (P /\ R) ) by XBOOLE_0:def 3;
( ( x in (dom P) /\ (dom R) or x in (rng P) /\ (rng R) ) implies ( ( x in dom P or x in rng P ) & ( x in dom R or x in rng R ) ) ) by XBOOLE_0:def 4;
then A2: ( ( x in (dom P) /\ (dom R) or x in (rng P) /\ (rng R) ) implies ( x in (dom P) \/ (rng P) & x in (dom R) \/ (rng R) ) ) by XBOOLE_0:def 3;
( dom (P /\ R) c= (dom P) /\ (dom R) & rng (P /\ R) c= (rng P) /\ (rng R) ) by XTUPLE_0:24, XTUPLE_0:28;
hence x in (field P) /\ (field R) by A1, A2, XBOOLE_0:def 4; :: thesis: verum