thus
( F_{4}() in F_{5}(F_{3}()) implies for b being Element of F_{2}() st b in F_{3}() holds

P_{1}[F_{4}(),b] )
:: thesis: ( ( for b being Element of F_{2}() st b in F_{3}() holds

P_{1}[F_{4}(),b] ) implies F_{4}() in F_{5}(F_{3}()) )_{2}() st b in F_{3}() holds

P_{1}[F_{4}(),b]
; :: thesis: F_{4}() in F_{5}(F_{3}())

hence F_{4}() in F_{5}(F_{3}())
by A1, A2; :: thesis: verum

P

P

proof

assume
for b being Element of F
defpred S_{1}[ set ] means P_{2}[$1,F_{3}()];

assume F_{4}() in F_{5}(F_{3}())
; :: thesis: for b being Element of F_{2}() st b in F_{3}() holds

P_{1}[F_{4}(),b]

then A3: F_{4}() in { a where a is Element of F_{1}() : S_{1}[a] }
by A1;

S_{1}[F_{4}()]
from LMOD_7:sch 6(A3);

hence for b being Element of F_{2}() st b in F_{3}() holds

P_{1}[F_{4}(),b]
by A2; :: thesis: verum

end;assume F

P

then A3: F

S

hence for b being Element of F

P

P

hence F