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