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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { F₂(v1) where v1 is Element of F₁() : P₁[v1] } or a in { F₂(v2) where v2 is Element of F₁() : P₂[v2] } )
assume a in { F₂(v1) where v1 is Element of F₁() : P₁[v1] } ; :: thesis: a in { F₂(v2) where v2 is Element of F₁() : P₂[v2] }
then consider V1 being Element of F₁() such that
A2: a = F₂(V1) and
A3: P₁[V1] ;
P₂[V1] by A1, A3;
hence a in { F₂(v2) where v2 is Element of F₁() : P₂[v2] } by A2; :: thesis: verum

end;

thus { F₂(v2) where v2 is Element of F₁() : P₂[v2] } c= { F₂(v1) where v1 is Element of F₁() : P₁[v1] } :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { F₂(v2) where v2 is Element of F₁() : P₂[v2] } or a in { F₂(v1) where v1 is Element of F₁() : P₁[v1] } )
assume a in { F₂(v1) where v1 is Element of F₁() : P₂[v1] } ; :: thesis: a in { F₂(v1) where v1 is Element of F₁() : P₁[v1] }
then consider V1 being Element of F₁() such that
A4: a = F₂(V1) and
A5: P₂[V1] ;
P₁[V1] by A1, A5;
hence a in { F₂(v1) where v1 is Element of F₁() : P₁[v1] } by A4; :: thesis: verum

end;