set A = { a where a is Element of F1() : ( P1[a] & P2[a] ) } ;
set A1 = { a1 where a1 is Element of F1() : P1[a1] } ;
set A2 = { a2 where a2 is Element of F1() : P2[a2] } ;
thus { a where a is Element of F1() : ( P1[a] & P2[a] ) } c= { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } :: according to XBOOLE_0:def 10 :: thesis: { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } c= { a where a is Element of F1() : ( P1[a] & P2[a] ) }
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } or x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } )
assume x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } ; :: thesis: x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] }
then consider a being Element of F1() such that
A1: x = a and
A2: ( P1[a] & P2[a] ) ;
 ( a in { a1 where a1 is Element of F1() : P1[a1] } & a in { a2 where a2 is Element of F1() : P2[a2] } ) by A2;
hence x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } by A1, XBOOLE_0:def 4; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } or x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } )
assume A3: x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } ; :: thesis: x in { a where a is Element of F1() : ( P1[a] & P2[a] ) }
then x in { a2 where a2 is Element of F1() : P2[a2] } by XBOOLE_0:def 4;
then A4: ex a being Element of F1() st
( x = a & P2[a] ) ;
x in { a1 where a1 is Element of F1() : P1[a1] } by A3, XBOOLE_0:def 4;
then ex a being Element of F1() st
( x = a & P1[a] ) ;
hence x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } by A4; :: thesis: verum