thus F₂() c= F₃() :: according to XBOOLE_0:def 10 :: thesis: F₃() c= F₂()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F₂() or x in F₃() )
assume A3: x in F₂() ; :: thesis: x in F₃()
then reconsider X = x as Element of F₁() by Lm3;
P₁[X] by A1, A3;
hence x in F₃() by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F₃() or x in F₂() )
assume A4: x in F₃() ; :: thesis: x in F₂()
then reconsider X = x as Element of F₁() by Lm3;
P₁[X] by A2, A4;
hence x in F₂() by A1; :: thesis: verum