thus { F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t] } c= { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] } :: according to XBOOLE_0:def 10 :: thesis: { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] } c= { F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t] } or x in { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] } )
assume x in { F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t] } ; :: thesis: x in { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] }
then consider s being Element of F1(), t being Element of F2() such that
A2: x = F3(s,t) and
A3: P2[s,t] ;
A4: P1[s,t] by A1, A3;
t = F4() by A1, A3;
hence x in { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] } by A2, A4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] } or x in { F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t] } )
assume x in { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] } ; :: thesis: x in { F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t] }
then consider s9 being Element of F1() such that
A5: x = F3(s9,F4()) and
A6: P1[s9,F4()] ;
 P2[s9,F4()] by A1, A6;
hence x in { F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t] } by A5; :: thesis: verum