thus
( F_{3}() in F_{1}() implies P_{1}[F_{3}()] )
:: thesis: ( P_{1}[F_{3}()] implies F_{3}() in F_{1}() )_{1}[F_{3}()]
; :: thesis: F_{3}() in F_{1}()

hence F_{3}() in F_{1}()
by A1; :: thesis: verum

proof

assume
P
assume
F_{3}() in F_{1}()
; :: thesis: P_{1}[F_{3}()]

then A2: F_{3}() in { a where a is Element of F_{2}() : P_{1}[a] }
by A1;

thus P_{1}[F_{3}()]
from LMOD_7:sch 6(A2); :: thesis: verum

end;then A2: F

thus P

hence F