thus { F₁() where a is Element of F₂() : P₁[a] } c= {F₁()} :: according to XBOOLE_0:def 10 :: thesis: {F₁()} c= { F₁() where a is Element of F₂() : P₁[a] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₁() where a is Element of F₂() : P₁[a] } or x in {F₁()} )
assume x in { F₁() where a is Element of F₂() : P₁[a] } ; :: thesis: x in {F₁()}
then ex a being Element of F₂() st
( x = F₁() & P₁[a] ) ;
hence x in {F₁()} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {F₁()} or x in { F₁() where a is Element of F₂() : P₁[a] } )
assume x in {F₁()} ; :: thesis: x in { F₁() where a is Element of F₂() : P₁[a] }
then x = F₁() by TARSKI:def 1;
hence x in { F₁() where a is Element of F₂() : P₁[a] } by A1; :: thesis: verum