let L be continuous LATTICE; :: thesis: for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds
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 )
let p be Element of L; :: thesis: ( uparrow (fininfs ((downarrow p) `)) misses waybelow p implies 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 ) )
assume A1: uparrow (fininfs ((downarrow p) `)) misses waybelow p ; :: thesis: 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 )
let A be non empty finite Subset of L; :: thesis: ( inf A << p implies ex a being Element of L st
( a in A & a <= p ) )
assume inf A << p ; :: thesis: ex a being Element of L st
( a in A & a <= p )
then inf A in waybelow p ;
then not inf A in uparrow (fininfs ((downarrow p) `)) by A1, XBOOLE_0:3;
then ( (downarrow p) ` c= uparrow (fininfs ((downarrow p) `)) & not A c= uparrow (fininfs ((downarrow p) `)) ) by WAYBEL_0:43, WAYBEL_0:62;
then not A c= (downarrow p) ` ;
then consider a being object such that
A2: a in A and
A3: not a in (downarrow p) ` ;
reconsider a = a as Element of L by A2;
take a ; :: thesis: ( a in A & a <= p )
a in downarrow p by A3, SUBSET_1:29;
hence ( a in A & a <= p ) by A2, WAYBEL_0:17; :: thesis: verum