thus F2() c= F3() :: according to XBOOLE_0:def 10 :: thesis: F3() c= F2()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F2() or x in F3() )
assume A3: x in F2() ; :: thesis: x in F3()
then reconsider X = x as Element of F1() by Lm3;
P1[X] by A1, A3;
hence x in F3() by A2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F3() or x in F2() )
assume A4: x in F3() ; :: thesis: x in F2()
then reconsider X = x as Element of F1() by Lm3;
P1[X] by A2, A4;
hence x in F2() by A1; :: thesis: verum