A3: for x being set st x in F₂() holds
x in F₁()

proof

let x be set ; :: thesis: ( x in F₂() implies x in F₁() )
assume x in F₂() ; :: thesis: x in F₁()
then P₁[x] by A2;
hence x in F₁() by A1; :: thesis: verum

end;

for x being set st x in F₁() holds
x in F₂()

proof

let x be set ; :: thesis: ( x in F₁() implies x in F₂() )
assume x in F₁() ; :: thesis: x in F₂()
then P₁[x] by A1;
hence x in F₂() by A2; :: thesis: verum

end;

hence F₁() = F₂() by A3, TARSKI:1; :: thesis: verum