set X = the carrier of T;

set L = BoolePoset ([#] T);

set F = a_filter N;

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 ;

hence a_filter N is proper by A1; :: thesis: a_filter N is filtered

let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def 2 :: thesis: ( not a in a_filter N or not b in a_filter N or ex b_{1} being Element of the carrier of (BoolePoset ([#] T)) st

( b_{1} in a_filter N & b_{1} <= a & b_{1} <= b ) )

assume that

A3: a in a_filter N and

A4: b in a_filter N ; :: thesis: ex b_{1} being Element of the carrier of (BoolePoset ([#] T)) st

( b_{1} in a_filter N & b_{1} <= a & b_{1} <= b )

N is_eventually_in a by A3, Th10;

then consider i1 being Element of N such that

A5: for j being Element of N st i1 <= j holds

N . j in a ;

N is_eventually_in b by A4, Th10;

then consider i2 being Element of N such that

A6: for j being Element of N st i2 <= j holds

N . j in b ;

take z = a "/\" b; :: thesis: ( z in a_filter N & z <= a & z <= b )

A7: z = a /\ b by YELLOW_1:17;

then A8: z c= b by XBOOLE_1:17;

consider i being Element of N such that

A9: i1 <= i and

A10: i2 <= i by YELLOW_6:def 3;

hence z in a_filter N by A1; :: thesis: ( z <= a & z <= b )

z c= a by A7, XBOOLE_1:17;

hence ( z <= a & z <= b ) by A8, YELLOW_1:2; :: thesis: verum

set L = BoolePoset ([#] T);

set F = a_filter N;

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 ;

now :: thesis: ( {} c= the carrier of T & not {} in a_filter N )

then
a_filter N <> bool the carrier of T
;thus
{} c= the carrier of T
; :: thesis: not {} in a_filter N

assume {} in a_filter N ; :: thesis: contradiction

then N is_eventually_in {} by Th10;

then consider i being Element of N such that

A2: for j being Element of N st i <= j holds

N . j in {} ;

ex j being Element of N st

( i <= j & i <= j ) by YELLOW_6:def 3;

hence contradiction by A2; :: thesis: verum

end;assume {} in a_filter N ; :: thesis: contradiction

then N is_eventually_in {} by Th10;

then consider i being Element of N such that

A2: for j being Element of N st i <= j holds

N . j in {} ;

ex j being Element of N st

( i <= j & i <= j ) by YELLOW_6:def 3;

hence contradiction by A2; :: thesis: verum

hence a_filter N is proper by A1; :: thesis: a_filter N is filtered

let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def 2 :: thesis: ( not a in a_filter N or not b in a_filter N or ex b

( b

assume that

A3: a in a_filter N and

A4: b in a_filter N ; :: thesis: ex b

( b

N is_eventually_in a by A3, Th10;

then consider i1 being Element of N such that

A5: for j being Element of N st i1 <= j holds

N . j in a ;

N is_eventually_in b by A4, Th10;

then consider i2 being Element of N such that

A6: for j being Element of N st i2 <= j holds

N . j in b ;

take z = a "/\" b; :: thesis: ( z in a_filter N & z <= a & z <= b )

A7: z = a /\ b by YELLOW_1:17;

then A8: z c= b by XBOOLE_1:17;

consider i being Element of N such that

A9: i1 <= i and

A10: i2 <= i by YELLOW_6:def 3;

now :: thesis: for j being Element of N st i <= j holds

N . j in a /\ b

then
N is_eventually_in z
by A7;N . j in a /\ b

let j be Element of N; :: thesis: ( i <= j implies N . j in a /\ b )

assume A11: i <= j ; :: thesis: N . j in a /\ b

then A12: N . j in b by A6, A10, ORDERS_2:3;

N . j in a by A5, A9, A11, ORDERS_2:3;

hence N . j in a /\ b by A12, XBOOLE_0:def 4; :: thesis: verum

end;assume A11: i <= j ; :: thesis: N . j in a /\ b

then A12: N . j in b by A6, A10, ORDERS_2:3;

N . j in a by A5, A9, A11, ORDERS_2:3;

hence N . j in a /\ b by A12, XBOOLE_0:def 4; :: thesis: verum

hence z in a_filter N by A1; :: thesis: ( z <= a & z <= b )

z c= a by A7, XBOOLE_1:17;

hence ( z <= a & z <= b ) by A8, YELLOW_1:2; :: thesis: verum