set X = the carrier of T;

set F = { A where A is Subset of T : N is_eventually_in A } ;

A1: { A where A is Subset of T : N is_eventually_in A } c= bool the carrier of T

.= RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def 1 ;

hence { A where A is Subset of T : N is_eventually_in A } is Subset of (BoolePoset ([#] T)) by A1; :: thesis: verum

set F = { A where A is Subset of T : N is_eventually_in A } ;

A1: { A where A is Subset of T : N is_eventually_in A } c= bool the carrier of T

proof

BoolePoset the carrier of T =
InclPoset (bool the carrier of T)
by YELLOW_1:4
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of T : N is_eventually_in A } or x in bool the carrier of T )

assume x in { A where A is Subset of T : N is_eventually_in A } ; :: thesis: x in bool the carrier of T

then ex A being Subset of T st

( x = A & N is_eventually_in A ) ;

hence x in bool the carrier of T ; :: thesis: verum

end;assume x in { A where A is Subset of T : N is_eventually_in A } ; :: thesis: x in bool the carrier of T

then ex A being Subset of T st

( x = A & N is_eventually_in A ) ;

hence x in bool the carrier of T ; :: thesis: verum

.= RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def 1 ;

hence { A where A is Subset of T : N is_eventually_in A } is Subset of (BoolePoset ([#] T)) by A1; :: thesis: verum