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 :: thesis: for x being object st x in uparrow (fininfs ((downarrow p) `)) holds
not x in waybelow p
let x be object ; :: 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 and
A5: b in fininfs ((downarrow p) `) by A3, WAYBEL_0:def 16;
assume x in waybelow p ; :: thesis: contradiction
then A6: a << p by WAYBEL_3:7;
then A7: b << p by A4, WAYBEL_3:2;
consider Y being finite Subset of ((downarrow p) `) such that
A8: b = "/\" (Y,L) and
ex_inf_of Y,L by A5;
reconsider Y = Y as finite Subset of L by XBOOLE_1:1;
per cases ( Y <> {} or Y = {} ) ;
suppose Y <> {} ; :: thesis: contradiction
then consider c being Element of L such that
A9: c in Y and
A10: c <= p by A2, A4, A8, A6, WAYBEL_3:2;
c in downarrow p by A10, WAYBEL_0:17;
then ( downarrow p misses (downarrow p) ` & c in (downarrow p) /\ ((downarrow p) `) ) by A9, XBOOLE_0:def 4, XBOOLE_1:79;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence uparrow (fininfs ((downarrow p) `)) misses waybelow p by XBOOLE_0:3; :: thesis: verum