A3: for x being object st x in F₂() holds
x in F₁() by A1, A2;
for x being object st x in F₁() holds
x in F₂() by A1, A2;
hence F₁() = F₂() by A3, TARSKI:2; :: thesis: verum