set X = the carrier of T;

set L = BoolePoset ([#] T);

set F = a_filter N;

N is_eventually_in [#] T

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

set L = BoolePoset ([#] T);

set F = a_filter N;

N is_eventually_in [#] T

proof

hence
not a_filter N is empty
by Th10; :: thesis: a_filter N is upper
set i = the Element of N;

take the Element of N ; :: according to WAYBEL_0:def 11 :: thesis: for b_{1} being Element of the carrier of N holds

( not the Element of N <= b_{1} or N . b_{1} in [#] T )

thus for b_{1} being Element of the carrier of N holds

( not the Element of N <= b_{1} or N . b_{1} in [#] T )
; :: thesis: verum

end;take the Element of N ; :: according to WAYBEL_0:def 11 :: thesis: for b

( not the Element of N <= b

thus for b

( not the Element of N <= b

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