thus { F₃(w) where w is Element of F₁() : w in {} } c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= { F₃(w) where w is Element of F₁() : w in {} }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { F₃(w) where w is Element of F₁() : w in {} } or a in {} )
assume A1: a in { F₃(w) where w is Element of F₁() : w in {} } ; :: thesis: a in {}
assume not a in {} ; :: thesis: contradiction
consider w being Element of F₁() such that
A2: ( a = F₃(w) & w in {} ) by A1;
thus contradiction by A2; :: thesis: verum

end;

thus {} c= { F₃(w) where w is Element of F₁() : w in {} } by XBOOLE_1:2; :: thesis: verum