set F = a_filter N;
set X = the carrier of T;
set L = BoolePoset ([#] T);
A1: 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 ;
N is_eventually_in [#] T

proof

consider i being Element of N;
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not i <= b₁ or N . b₁ in [#] T )
thus for b₁ being Element of the carrier of N holds
( not i <= b₁ or N . b₁ in [#] T ) ; :: thesis: verum

end;

hence not a_filter N is empty by Th11; :: thesis: a_filter N is upper
let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def 20 :: thesis: ( not a in a_filter N or not a <= b or b in a_filter N )
assume a in a_filter N ; :: thesis: ( not a <= b or b in a_filter N )
then A3: N is_eventually_in a by Th11;
assume a <= b ; :: thesis: b in a_filter N
then a c= b by YELLOW_1:2;
then ( b is Subset of T & N is_eventually_in b ) by A1, A3, WAYBEL_0:8;
hence b in a_filter N ; :: thesis: verum