let L be continuous LATTICE; :: thesis: for p being Element of L st ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) ) holds
uparrow (fininfs ((downarrow p) ` )) misses waybelow p
let p be Element of L; :: thesis: ( ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) ) implies uparrow (fininfs ((downarrow p) ` )) misses waybelow p )
assume that
A1: ( p <> Top L or not Top L is compact ) and
A2: for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) ; :: thesis: uparrow (fininfs ((downarrow p) ` )) misses waybelow p

now

let x be set ; :: thesis: ( x in uparrow (fininfs ((downarrow p) ` )) implies not x in waybelow p )
assume A3: x in uparrow (fininfs ((downarrow p) ` )) ; :: thesis: not x in waybelow p
then reconsider a = x as Element of L ;
consider b being Element of L such that
A4: ( a >= b & b in fininfs ((downarrow p) ` ) ) by A3, WAYBEL_0:def 16;
consider Y being finite Subset of ((downarrow p) ` ) such that
A5: ( b = "/\" Y,L & ex_inf_of Y,L ) by A4;
reconsider Y = Y as finite Subset of L by XBOOLE_1:1;
assume x in waybelow p ; :: thesis: contradiction
then a << p by WAYBEL_3:7;
then A6: b << p by A4, WAYBEL_3:2;

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

suppose Y <> {} ; :: thesis: contradiction

then consider c being Element of L such that
A7: ( c in Y & c <= p ) by A2, A5, A6;
A8: downarrow p misses (downarrow p) ` by XBOOLE_1:79;
( c in (downarrow p) ` & c in downarrow p ) by A7, WAYBEL_0:17;
then c in (downarrow p) /\ ((downarrow p) ` ) by XBOOLE_0:def 4;
hence contradiction by A8, XBOOLE_0:def 7; :: thesis: verum

end;

suppose A9: Y = {} ; :: thesis: contradiction

then ( b = Top L & b <= p & p <= Top L ) by A5, A6, WAYBEL_3:1, YELLOW_0:45;
then p = Top L by ORDERS_2:25;
hence contradiction by A1, A5, A6, A9, WAYBEL_3:def 2; :: thesis: verum

end;

end;

end;

hence uparrow (fininfs ((downarrow p) ` )) misses waybelow p by XBOOLE_0:3; :: thesis: verum