for x being Element of F₁() holds
( x in F₂() iff x in F₃() ) by A1, A2;
hence F₂() = F₃() by Th2; :: thesis: verum