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

let x be object ; :: thesis: ( x in COMPLEMENT F₂() implies x in { F₄(a) where a is Element of F₁() : a in F₃() } )
assume A2: x in COMPLEMENT F₂() ; :: thesis: x in { F₄(a) where a is Element of F₁() : a in F₃() }
then reconsider y = x as Subset of F₁() ;
y ` in F<sub>2</sub>() by A2, SETFAM_1:def 7;
then A3: ex b being Element of F<sub>1</sub>() st
( y ` = F₄(b) ` & b in F<sub>3</sub>() ) by A1;
x = (y `) ` ;
hence x in { F₄(a) where a is Element of F₁() : a in F₃() } by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₄(a) where a is Element of F₁() : a in F₃() } or x in COMPLEMENT F₂() )
assume x in { F₄(a) where a is Element of F₁() : a in F₃() } ; :: thesis: x in COMPLEMENT F₂()
then consider a being Element of F₁() such that
A4: x = F₄(a) and
A5: a in F₃() ;
F₄(a) ` in F₂() by A1, A5;
hence x in COMPLEMENT F₂() by A4, SETFAM_1:def 7; :: thesis: verum