thus
{ F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : P_{2}[s,t] } c= { F_{3}(s9,F_{4}()) where s9 is Element of F_{1}() : P_{1}[s9,F_{4}()] }
:: according to XBOOLE_0:def 10 :: thesis: { F_{3}(s9,F_{4}()) where s9 is Element of F_{1}() : P_{1}[s9,F_{4}()] } c= { F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : P_{2}[s,t] } _{3}(s9,F_{4}()) where s9 is Element of F_{1}() : P_{1}[s9,F_{4}()] } or x in { F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : P_{2}[s,t] } )

assume x in { F_{3}(s9,F_{4}()) where s9 is Element of F_{1}() : P_{1}[s9,F_{4}()] }
; :: thesis: x in { F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : P_{2}[s,t] }

then consider s9 being Element of F_{1}() such that

A5: x = F_{3}(s9,F_{4}())
and

A6: P_{1}[s9,F_{4}()]
;

P_{2}[s9,F_{4}()]
by A1, A6;

hence x in { F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : P_{2}[s,t] }
by A5; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : P_{2}[s,t] } or x in { F_{3}(s9,F_{4}()) where s9 is Element of F_{1}() : P_{1}[s9,F_{4}()] } )

assume x in { F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : P_{2}[s,t] }
; :: thesis: x in { F_{3}(s9,F_{4}()) where s9 is Element of F_{1}() : P_{1}[s9,F_{4}()] }

then consider s being Element of F_{1}(), t being Element of F_{2}() such that

A2: x = F_{3}(s,t)
and

A3: P_{2}[s,t]
;

A4: P_{1}[s,t]
by A1, A3;

t = F_{4}()
by A1, A3;

hence x in { F_{3}(s9,F_{4}()) where s9 is Element of F_{1}() : P_{1}[s9,F_{4}()] }
by A2, A4; :: thesis: verum

end;assume x in { F

then consider s being Element of F

A2: x = F

A3: P

A4: P

t = F

hence x in { F

assume x in { F

then consider s9 being Element of F

A5: x = F

A6: P

P

hence x in { F