set X = the carrier of T;
set L = BoolePoset ([#] T);
set F = a_filter N;
N is_eventually_in [#] T
proof
set i = the Element of N;
take the Element of N ; :: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of N holds
( not the Element of N <= b1 or N . b1 in [#] T )
thus for b1 being Element of the carrier of N holds
( not the Element of N <= b1 or N . b1 in [#] T ) ; :: thesis: verum
end;
hence not a_filter N is empty by Th10; :: 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 A1: N is_eventually_in a by Th10;
assume a <= b ; :: thesis: b in a_filter N
then a c= b by YELLOW_1:2;
then A2: N is_eventually_in b by A1, WAYBEL_0:8;
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 b in a_filter N by A2; :: thesis: verum