let L be lower-bounded continuous LATTICE; :: thesis: for B being join-closed Subset of L st Bottom L in B & ( for x, y being Element of L st x << y holds

ex b being Element of L st

( b in B & x <= b & b << y ) ) holds

( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) )

let B be join-closed Subset of L; :: thesis: ( Bottom L in B & ( for x, y being Element of L st x << y holds

ex b being Element of L st

( b in B & x <= b & b << y ) ) implies ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) ) )

assume A1: Bottom L in B ; :: thesis: ( ex x, y being Element of L st

( x << y & ( for b being Element of L holds

( not b in B or not x <= b or not b << y ) ) ) or ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) ) )

assume A2: for x, y being Element of L st x << y holds

ex b being Element of L st

( b in B & x <= b & b << y ) ; :: thesis: ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) )

thus the carrier of (CompactSublatt L) c= B :: thesis: for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y )

( b in B & not b <= x & b <= y ) )

assume A7: not y <= x ; :: thesis: ex b being Element of L st

( b in B & not b <= x & b <= y )

B is CLbasis of L by A1, A2, Th47;

then consider b being Element of L such that

A8: b in B and

A9: not b <= x and

A10: b << y by A7, Th46;

take b ; :: thesis: ( b in B & not b <= x & b <= y )

thus ( b in B & not b <= x & b <= y ) by A8, A9, A10, WAYBEL_3:1; :: thesis: verum

ex b being Element of L st

( b in B & x <= b & b << y ) ) holds

( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) )

let B be join-closed Subset of L; :: thesis: ( Bottom L in B & ( for x, y being Element of L st x << y holds

ex b being Element of L st

( b in B & x <= b & b << y ) ) implies ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) ) )

assume A1: Bottom L in B ; :: thesis: ( ex x, y being Element of L st

( x << y & ( for b being Element of L holds

( not b in B or not x <= b or not b << y ) ) ) or ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) ) )

assume A2: for x, y being Element of L st x << y holds

ex b being Element of L st

( b in B & x <= b & b << y ) ; :: thesis: ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) )

thus the carrier of (CompactSublatt L) c= B :: thesis: for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y )

proof

let x, y be Element of L; :: thesis: ( not y <= x implies ex b being Element of L st
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of (CompactSublatt L) or z in B )

assume A3: z in the carrier of (CompactSublatt L) ; :: thesis: z in B

the carrier of (CompactSublatt L) c= the carrier of L by YELLOW_0:def 13;

then reconsider z1 = z as Element of L by A3;

z1 is compact by A3, WAYBEL_8:def 1;

then z1 << z1 by WAYBEL_3:def 2;

then consider b being Element of L such that

A4: b in B and

A5: z1 <= b and

A6: b << z1 by A2;

b <= z1 by A6, WAYBEL_3:1;

hence z in B by A4, A5, YELLOW_0:def 3; :: thesis: verum

end;assume A3: z in the carrier of (CompactSublatt L) ; :: thesis: z in B

the carrier of (CompactSublatt L) c= the carrier of L by YELLOW_0:def 13;

then reconsider z1 = z as Element of L by A3;

z1 is compact by A3, WAYBEL_8:def 1;

then z1 << z1 by WAYBEL_3:def 2;

then consider b being Element of L such that

A4: b in B and

A5: z1 <= b and

A6: b << z1 by A2;

b <= z1 by A6, WAYBEL_3:1;

hence z in B by A4, A5, YELLOW_0:def 3; :: thesis: verum

( b in B & not b <= x & b <= y ) )

assume A7: not y <= x ; :: thesis: ex b being Element of L st

( b in B & not b <= x & b <= y )

B is CLbasis of L by A1, A2, Th47;

then consider b being Element of L such that

A8: b in B and

A9: not b <= x and

A10: b << y by A7, Th46;

take b ; :: thesis: ( b in B & not b <= x & b <= y )

thus ( b in B & not b <= x & b <= y ) by A8, A9, A10, WAYBEL_3:1; :: thesis: verum