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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in { F₃(w) where w is Element of F₁() : w in {} } or a in {} )
assume a in { F₃(w) where w is Element of F₁() : w in {} } ; :: thesis: a in {}
then A1: ex w being Element of F₁() st
( a = F₃(w) & w in {} ) ;
assume not a in {} ; :: thesis: contradiction
thus contradiction by A1; :: thesis: verum

end;

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