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
proof
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;
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4
.= 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