let L be lower-bounded continuous LATTICE; :: thesis: for B being join-closed Subset of L st Bottom L in B holds

( B is CLbasis of L iff ( 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 implies ( B is CLbasis of L iff ( 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: ( B is CLbasis of L iff ( 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 ( B is CLbasis of L 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 ) ) ) ) :: 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 ) ) implies B is CLbasis of L )

the carrier of (CompactSublatt L) c= B and

A2: 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 ) ; :: thesis: B is CLbasis of L

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 ) by A2, Lm3;

hence B is CLbasis of L by Th46; :: thesis: verum

( B is CLbasis of L iff ( 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 implies ( B is CLbasis of L iff ( 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: ( B is CLbasis of L iff ( 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 ( B is CLbasis of L 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 ) ) ) ) :: 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 ) ) implies B is CLbasis of L )

proof

assume that
assume
B is CLbasis of L
; :: 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 ) ) )

then 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 ) by A1, Th47;

hence ( 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 ) ) ) by A1, Lm2; :: thesis: verum

end;ex b being Element of L st

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

then 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 ) by A1, Th47;

hence ( 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 ) ) ) by A1, Lm2; :: thesis: verum

the carrier of (CompactSublatt L) c= B and

A2: 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 ) ; :: thesis: B is CLbasis of L

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 ) by A2, Lm3;

hence B is CLbasis of L by Th46; :: thesis: verum