set X = { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] } ;

_{2}() such that A2:
for j being Element of F_{2}() st i <= j holds

P_{1}[F_{2}() . j]
; :: thesis: F_{2}() is_eventually_in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] }

take i ; :: according to WAYBEL_0:def 11 :: thesis: for j being Element of F_{2}() st i <= j holds

F_{2}() . j in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] }

let j be Element of F_{2}(); :: thesis: ( i <= j implies F_{2}() . j in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] } )

assume i <= j ; :: thesis: F_{2}() . j in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] }

then P_{1}[F_{2}() . j]
by A2;

hence F_{2}() . j in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] }
; :: thesis: verum

hereby :: thesis: ( ex i being Element of F_{2}() st

for j being Element of F_{2}() st i <= j holds

P_{1}[F_{2}() . j] implies F_{2}() is_eventually_in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] } )

given i being Element of Ffor j being Element of F

P

assume
F_{2}() is_eventually_in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] }
; :: thesis: ex i being Element of F_{2}() st

for j being Element of F_{2}() st i <= j holds

P_{1}[F_{2}() . j]

then consider i being Element of F_{2}() such that

A1: for j being Element of F_{2}() st i <= j holds

F_{2}() . j in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] }
;

take i = i; :: thesis: for j being Element of F_{2}() st i <= j holds

P_{1}[F_{2}() . j]

let j be Element of F_{2}(); :: thesis: ( i <= j implies P_{1}[F_{2}() . j] )

assume i <= j ; :: thesis: P_{1}[F_{2}() . j]

then F_{2}() . j in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] }
by A1;

then ex k being Element of F_{2}() st

( F_{2}() . j = F_{2}() . k & P_{1}[F_{2}() . k] )
;

hence P_{1}[F_{2}() . j]
; :: thesis: verum

end;for j being Element of F

P

then consider i being Element of F

A1: for j being Element of F

F

take i = i; :: thesis: for j being Element of F

P

let j be Element of F

assume i <= j ; :: thesis: P

then F

then ex k being Element of F

( F

hence P

P

take i ; :: according to WAYBEL_0:def 11 :: thesis: for j being Element of F

F

let j be Element of F

assume i <= j ; :: thesis: F

then P

hence F