set X = { (F2() . k) where k is Element of F2() : P1[F2() . k] } ;
hereby :: thesis: ( ex i being Element of F2() st
for j being Element of F2() st i <= j holds
P1[F2() . j] implies F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } )
assume F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } ; :: thesis: ex i being Element of F2() st
for j being Element of F2() st i <= j holds
P1[F2() . j]
then consider i being Element of F2() such that
A1: for j being Element of F2() st i <= j holds
F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } by Def11;
take i = i; :: thesis: for j being Element of F2() st i <= j holds
P1[F2() . j]
let j be Element of F2(); :: thesis: ( i <= j implies P1[F2() . j] )
assume i <= j ; :: thesis: P1[F2() . j]
then F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } by A1;
then ex k being Element of F2() st
( F2() . j = F2() . k & P1[F2() . k] ) ;
hence P1[F2() . j] ; :: thesis: verum
end;
given i being Element of F2() such that A2: for j being Element of F2() st i <= j holds
P1[F2() . j] ; :: thesis: F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] }
take i ; :: according to WAYBEL_0:def 11 :: thesis: for j being Element of F2() st i <= j holds
F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] }
let j be Element of F2(); :: thesis: ( i <= j implies F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } )
assume i <= j ; :: thesis: F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] }
then P1[F2() . j] by A2;
hence F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } ; :: thesis: verum