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) ) )
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 & u in fininfs (I \/ X) ) by WAYBEL_0:def 16;
consider Y being finite Subset of (I \/ X) such that
A2: ( u = "/\" Y,L & ex_inf_of Y,L ) by A1;
Y \ X c= I

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Y \ X or a in I )
assume a in Y \ X ; :: thesis: a in I
then ( a in Y & not a in X ) by XBOOLE_0:def 5;
hence a in I by XBOOLE_0:def 3; :: thesis: verum

end;

then reconsider Z = Y \ X as finite Subset of I ;
reconsider Z' = Z, Y' = Y as finite Subset of L by XBOOLE_1:1;
reconsider ZX = Z' \/ X as finite Subset of L ;
consider i being Element of I;
reconsider i = i as Element of L ;

per cases ( Z = {} or Z <> {} ) ;

suppose Z = {} ; :: thesis: ex a being Element of L st
( a in I & x >= a "/\" (inf X) )

then ( Y c= X & ex_inf_of X,L & ex_inf_of Y',L ) by A2, XBOOLE_1:37, YELLOW_0:55;
then ( u >= inf X & inf X >= i "/\" (inf X) ) by A2, YELLOW_0:23, YELLOW_0:35;
then A3: u >= i "/\" (inf X) by ORDERS_2:26;
take i ; :: thesis: ( i in I & x >= i "/\" (inf X) )
thus ( i in I & x >= i "/\" (inf X) ) by A1, A3, ORDERS_2:26; :: thesis: verum

end;

suppose A4: Z <> {} ; :: thesis: ex a being Element of L st
( a in I & x >= a "/\" (inf X) )

then A5: ( "/\" Z,L in I & ex_inf_of Z',L & ex_inf_of X,L & ex_inf_of ZX,L ) by WAYBEL_0:43, YELLOW_0:55;
then A6: inf (Z' \/ X) = (inf Z') "/\" (inf X) by YELLOW_0:37;
Y c= Y \/ X by XBOOLE_1:7;
then Y c= Z' \/ X by XBOOLE_1:39;
then A7: inf Y' >= inf ZX by A2, A5, YELLOW_0:35;
take i = inf Z'; :: thesis: ( i in I & x >= i "/\" (inf X) )
thus ( i in I & x >= i "/\" (inf X) ) by A1, A2, A4, A6, A7, ORDERS_2:26, WAYBEL_0:43; :: thesis: verum

end;

end;