A3: for x being object st x in F2() holds
x in F1()
proof
let x be object ; :: thesis: ( x in F2() implies x in F1() )
reconsider x = x as set by TARSKI:1;
( x in F2() implies x in F1() ) by A1, A2;
hence ( x in F2() implies x in F1() ) ; :: thesis: verum
end;
for x being object st x in F1() holds
x in F2()
proof
let x be object ; :: thesis: ( x in F1() implies x in F2() )
reconsider x = x as set by TARSKI:1;
( x in F1() implies x in F2() ) by A1, A2;
hence ( x in F1() implies x in F2() ) ; :: thesis: verum
end;
hence F1() = F2() by A3, TARSKI:2; :: thesis: verum