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 ;

now

thus {} c= the carrier of T by XBOOLE_1:2; :: thesis: not {} in a_filter N
assume {} in a_filter N ; :: thesis: contradiction
then N is_eventually_in {} by Th11;
then consider i being Element of N such that
A3: for j being Element of N st i <= j holds
N . j in {} by WAYBEL_0:def 11;
consider j being Element of N such that
A4: ( i <= j & i <= j ) by YELLOW_6:def 5;
thus contradiction by A3, A4; :: thesis: verum

end;

then a_filter N <> bool the carrier of T ;
hence a_filter N is proper by A1, SUBSET_1:def 7; :: 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₁ being Element of the carrier of (BoolePoset ([#] T)) st
( b₁ in a_filter N & b₁ <= a & b₁ <= b ) )
assume ( a in a_filter N & b in a_filter N ) ; :: thesis: ex b₁ being Element of the carrier of (BoolePoset ([#] T)) st
( b₁ in a_filter N & b₁ <= a & b₁ <= b )
then A5: ( N is_eventually_in a & N is_eventually_in b ) by Th11;
then consider i1 being Element of N such that
A6: for j being Element of N st i1 <= j holds
N . j in a by WAYBEL_0:def 11;
consider i2 being Element of N such that
A7: for j being Element of N st i2 <= j holds
N . j in b by A5, WAYBEL_0:def 11;
consider i being Element of N such that
A8: ( i1 <= i & i2 <= i ) by YELLOW_6:def 5;
take z = a "/\" b; :: thesis: ( z in a_filter N & z <= a & z <= b )
A9: ( z = a /\ b & z is Subset of T ) by A1, YELLOW_1:17;

now

let j be Element of N; :: thesis: ( i <= j implies N . j in a /\ b )
assume i <= j ; :: thesis: N . j in a /\ b
then ( i1 <= j & i2 <= j ) by A8, ORDERS_2:26;
then ( N . j in a & N . j in b ) by A6, A7;
hence N . j in a /\ b by XBOOLE_0:def 4; :: thesis: verum

end;

then N is_eventually_in z by A9, WAYBEL_0:def 11;
hence z in a_filter N by A1; :: thesis: ( z <= a & z <= b )
( z c= a & z c= b ) by A9, XBOOLE_1:17;
hence ( z <= a & z <= b ) by YELLOW_1:2; :: thesis: verum