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

assume x in { F_{3}(F_{4}(a)) where a is Element of F_{1}() : P_{1}[a] }
; :: thesis: x in { F_{3}(a) where a is Element of F_{2}() : a in { F_{4}(b) where b is Element of F_{1}() : P_{1}[b] } }

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

A3: x = F_{3}(F_{4}(a))
and

A4: P_{1}[a]
;

F_{4}(a) in { F_{4}(b) where b is Element of F_{1}() : P_{1}[b] }
by A4;

hence x in { F_{3}(a) where a is Element of F_{2}() : a in { F_{4}(b) where b is Element of F_{1}() : P_{1}[b] } }
by A3; :: 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}(a) where a is Element of F_{2}() : a in { F_{4}(b) where b is Element of F_{1}() : P_{1}[b] } } or x in { F_{3}(F_{4}(a)) where a is Element of F_{1}() : P_{1}[a] } )

assume x in { F_{3}(a) where a is Element of F_{2}() : a in { F_{4}(b) where b is Element of F_{1}() : P_{1}[b] } }
; :: thesis: x in { F_{3}(F_{4}(a)) where a is Element of F_{1}() : P_{1}[a] }

then consider a being Element of F_{2}() such that

A1: x = F_{3}(a)
and

A2: a in { F_{4}(b) where b is Element of F_{1}() : P_{1}[b] }
;

ex b being Element of F_{1}() st

( a = F_{4}(b) & P_{1}[b] )
by A2;

hence x in { F_{3}(F_{4}(a)) where a is Element of F_{1}() : P_{1}[a] }
by A1; :: thesis: verum

end;assume x in { F

then consider a being Element of F

A1: x = F

A2: a in { F

ex b being Element of F

( a = F

hence x in { F

assume x in { F

then consider a being Element of F

A3: x = F

A4: P

F

hence x in { F