let L be continuous LATTICE; :: thesis: ( Top L is compact implies ( ( for A being non empty finite Subset of L st inf A << Top L holds
ex a being Element of L st
( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) ) )

assume A1: Top L << Top L ; :: according to WAYBEL_3:def 2 :: thesis: ( ( for A being non empty finite Subset of L st inf A << Top L holds
ex a being Element of L st
( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) )

A2: now :: thesis: ex x being Element of the carrier of L st
( x in uparrow (fininfs ((downarrow (Top L)) `)) & x in waybelow (Top L) )
end;
hereby :: thesis: uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L)
let A be non empty finite Subset of L; :: thesis: ( inf A << Top L implies ex a being Element of L st
( a in A & a <= Top L ) )

assume inf A << Top L ; :: thesis: ex a being Element of L st
( a in A & a <= Top L )

set a = the Element of A;
reconsider a = the Element of A as Element of L ;
take a = a; :: thesis: ( a in A & a <= Top L )
thus ( a in A & a <= Top L ) by YELLOW_0:45; :: thesis: verum
end;
thus uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) by ; :: thesis: verum