hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { F₄(a) where a is Element of F₁() : a in F₃() } c= F₂()

let x be set ; :: thesis: ( x in F₂() implies x in { F₄(b) where b is Element of F₁() : b in F₃() } )
assume A3: x in F₂() ; :: thesis: x in { F₄(b) where b is Element of F₁() : b in F₃() }
then reconsider a = x as Element of F₁() ;
A4: F₄(a) in F₃() by A1, A3;
F₄(F₄(a)) = a by A2;
hence x in { F₄(b) where b is Element of F₁() : b in F₃() } by A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₄(a) where a is Element of F₁() : a in F₃() } or x in F₂() )
assume x in { F₄(b) where b is Element of F₁() : b in F₃() } ; :: thesis: x in F₂()
then consider b being Element of F₁() such that
A5: x = F₄(b) and
A6: b in F₃() ;
ex a being Element of F₁() st
( b = F₄(a) & a in F₂() ) by A1, A6;
hence x in F₂() by A2, A5; :: thesis: verum