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

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

( 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;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

hereby :: thesis: uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L)

thus
uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L)
by A2, XBOOLE_0:3; :: thesis: verumlet 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;( 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