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 ;
now :: thesis: ( {} c= the carrier of T & not {} in a_filter N )
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;
then a_filter N <> bool the carrier of T ;
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 b1 being Element of the carrier of (BoolePoset ([#] T)) st
( b1 in a_filter N & b1 <= a & b1 <= b ) )
assume that
A3: a in a_filter N and
A4: b in a_filter N ; :: thesis: ex b1 being Element of the carrier of (BoolePoset ([#] T)) st
( b1 in a_filter N & b1 <= a & b1 <= 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
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;
then N is_eventually_in z by A7;
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