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) )

take x = Top L; :: thesis: ( x in uparrow (fininfs ((downarrow (Top L)) `)) & x in waybelow (Top L) )
thus x in uparrow (fininfs ((downarrow (Top L)) `)) by WAYBEL_4:22; :: thesis: x in waybelow (Top L)
thus x in waybelow (Top L) by A1; :: thesis: verum

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 A2, XBOOLE_0:3; :: thesis: verum