for x being Element of F₁() holds
( x in F₂() iff x in F₃() )

proof

let x be Element of F₁(); :: thesis: ( x in F₂() iff x in F₃() )

hereby :: 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;

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

end;

hence F₂() = F₃() by Th8; :: thesis: verum