thus
{ st1 where st1 is Element of F_{3}() : ( st1 in { F_{4}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] } & P_{2}[st1] ) } c= { F_{4}(s2,t2) where s2 is Element of F_{1}(), t2 is Element of F_{2}() : ( P_{1}[s2,t2] & P_{2}[F_{4}(s2,t2)] ) }
:: according to XBOOLE_0:def 10 :: thesis: { F_{4}(s2,t2) where s2 is Element of F_{1}(), t2 is Element of F_{2}() : ( P_{1}[s2,t2] & P_{2}[F_{4}(s2,t2)] ) } c= { st1 where st1 is Element of F_{3}() : ( st1 in { F_{4}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] } & P_{2}[st1] ) } _{4}(s2,t2) where s2 is Element of F_{1}(), t2 is Element of F_{2}() : ( P_{1}[s2,t2] & P_{2}[F_{4}(s2,t2)] ) } or x in { st1 where st1 is Element of F_{3}() : ( st1 in { F_{4}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] } & P_{2}[st1] ) } )

assume x in { F_{4}(s2,t2) where s2 is Element of F_{1}(), t2 is Element of F_{2}() : ( P_{1}[s2,t2] & P_{2}[F_{4}(s2,t2)] ) }
; :: thesis: x in { st1 where st1 is Element of F_{3}() : ( st1 in { F_{4}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] } & P_{2}[st1] ) }

then consider s2 being Element of F_{1}(), t2 being Element of F_{2}() such that

A4: x = F_{4}(s2,t2)
and

A5: P_{1}[s2,t2]
and

A6: P_{2}[F_{4}(s2,t2)]
;

F_{4}(s2,t2) in { F_{4}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] }
by A5;

hence x in { st1 where st1 is Element of F_{3}() : ( st1 in { F_{4}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] } & P_{2}[st1] ) }
by A4, A6; :: 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 { st1 where st1 is Element of F_{3}() : ( st1 in { F_{4}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] } & P_{2}[st1] ) } or x in { F_{4}(s2,t2) where s2 is Element of F_{1}(), t2 is Element of F_{2}() : ( P_{1}[s2,t2] & P_{2}[F_{4}(s2,t2)] ) } )

assume x in { st1 where st1 is Element of F_{3}() : ( st1 in { F_{4}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] } & P_{2}[st1] ) }
; :: thesis: x in { F_{4}(s2,t2) where s2 is Element of F_{1}(), t2 is Element of F_{2}() : ( P_{1}[s2,t2] & P_{2}[F_{4}(s2,t2)] ) }

then consider st1 being Element of F_{3}() such that

A1: x = st1 and

A2: st1 in { F_{4}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] }
and

A3: P_{2}[st1]
;

ex s1 being Element of F_{1}() ex t1 being Element of F_{2}() st

( st1 = F_{4}(s1,t1) & P_{1}[s1,t1] )
by A2;

hence x in { F_{4}(s2,t2) where s2 is Element of F_{1}(), t2 is Element of F_{2}() : ( P_{1}[s2,t2] & P_{2}[F_{4}(s2,t2)] ) }
by A1, A3; :: thesis: verum

end;assume x in { st1 where st1 is Element of F

then consider st1 being Element of F

A1: x = st1 and

A2: st1 in { F

A3: P

ex s1 being Element of F

( st1 = F

hence x in { F

assume x in { F

then consider s2 being Element of F

A4: x = F

A5: P

A6: P

F

hence x in { st1 where st1 is Element of F