let L be with_infima Poset; :: thesis: for F being Filter of L
for X being non empty finite Subset of L
for x being Element of L st x in uparrow (fininfs (F \/ X)) holds
ex a being Element of L st
( a in F & x >= a "/\" (inf X) )
let I be Filter of L; :: thesis: for X being non empty finite Subset of L
for x being Element of L st x in uparrow (fininfs (I \/ X)) holds
ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
let X be non empty finite Subset of L; :: thesis: for x being Element of L st x in uparrow (fininfs (I \/ X)) holds
ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
let x be Element of L; :: thesis: ( x in uparrow (fininfs (I \/ X)) implies ex a being Element of L st
( a in I & x >= a "/\" (inf X) ) )
set i = the Element of I;
reconsider i = the Element of I as Element of L ;
assume x in uparrow (fininfs (I \/ X)) ; :: thesis: ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
then consider u being Element of L such that
A1: u <= x and
A2: u in fininfs (I \/ X) by WAYBEL_0:def 16;
consider Y being finite Subset of (I \/ X) such that
A3: u = "/\" (Y,L) and
A4: ex_inf_of Y,L by A2;
Y \ X c= I
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y \ X or a in I )
assume A5: a in Y \ X ; :: thesis: a in I
then not a in X by XBOOLE_0:def 5;
hence a in I by A5, XBOOLE_0:def 3; :: thesis: verum
end;
then reconsider Z = Y \ X as finite Subset of I ;
reconsider Z9 = Z, Y9 = Y as finite Subset of L by XBOOLE_1:1;
reconsider ZX = Z9 \/ X as finite Subset of L ;
per cases ( Z = {} or Z <> {} ) ;
suppose A6: Z = {} ; :: thesis: ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
A7: inf X >= i "/\" (inf X) by YELLOW_0:23;
take i ; :: thesis: ( i in I & x >= i "/\" (inf X) )
A8: ex_inf_of X,L by YELLOW_0:55;
Y c= X by A6, XBOOLE_1:37;
then u >= inf X by A3, A4, A8, YELLOW_0:35;
then u >= i "/\" (inf X) by A7, ORDERS_2:3;
hence ( i in I & x >= i "/\" (inf X) ) by A1, ORDERS_2:3; :: thesis: verum
end;
suppose A9: Z <> {} ; :: thesis: ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
take inf Z9 ; :: thesis: ( inf Z9 in I & x >= (inf Z9) "/\" (inf X) )
A10: ex_inf_of X,L by YELLOW_0:55;
A11: ex_inf_of ZX,L by YELLOW_0:55;
Y c= Y \/ X by XBOOLE_1:7;
then Y c= Z9 \/ X by XBOOLE_1:39;
then A12: inf Y9 >= inf ZX by A4, A11, YELLOW_0:35;
ex_inf_of Z9,L by A9, YELLOW_0:55;
then inf (Z9 \/ X) = (inf Z9) "/\" (inf X) by A10, A11, YELLOW_0:37;
hence ( inf Z9 in I & x >= (inf Z9) "/\" (inf X) ) by A1, A3, A9, A12, ORDERS_2:3, WAYBEL_0:43; :: thesis: verum
end;
end;