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()] }
XBOOLE_0:def 10 { 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 ;
TARSKI:def 3 ( 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] }
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( 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()] }
; 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; verum