let A be Subset of S; :: according to YELLOW19:def 5 :: thesis: ( a_net F is_eventually_in A or a_net F is_eventually_in A ` )

F is prime by WAYBEL_7:22;

then A1: ( ( ( A is empty or not A is empty ) & ( A ` is empty or not A ` is empty ) & A in F ) or A ` in F ) by WAYBEL_7:21;

({} S) ` = [#] S ;

then ( A ` = {} S implies A = [#] S ) ;

hence ( a_net F is_eventually_in A or a_net F is_eventually_in A ` ) by A1, Th15, YELLOW_6:20; :: thesis: verum

F is prime by WAYBEL_7:22;

then A1: ( ( ( A is empty or not A is empty ) & ( A ` is empty or not A ` is empty ) & A in F ) or A ` in F ) by WAYBEL_7:21;

({} S) ` = [#] S ;

then ( A ` = {} S implies A = [#] S ) ;

hence ( a_net F is_eventually_in A or a_net F is_eventually_in A ` ) by A1, Th15, YELLOW_6:20; :: thesis: verum