let T be non empty TopSpace; :: thesis: for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds
for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T
let L1 be continuous sup-Semilattice; :: thesis: ( InclPoset the topology of T = L1 implies for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T )
assume A1: InclPoset the topology of T = L1 ; :: thesis: for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T
let B1 be with_bottom CLbasis of L1; :: thesis: B1 is Basis of T
B1 c= the carrier of L1 ;
then B1 c= the topology of T by A1, YELLOW_1:1;
then reconsider B2 = B1 as Subset-Family of T by XBOOLE_1:1;
A2: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B2 & p in a & a c= A )

proof

let A be Subset of T; :: thesis: ( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in B2 & p in a & a c= A ) )
assume A is open ; :: thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in B2 & p in a & a c= A )
then A in the topology of T by PRE_TOPC:def 2;
then reconsider A1 = A as Element of L1 by A1, YELLOW_1:1;
let p be Point of T; :: thesis: ( p in A implies ex a being Subset of T st
( a in B2 & p in a & a c= A ) )
assume A3: p in A ; :: thesis: ex a being Subset of T st
( a in B2 & p in a & a c= A )
A1 = sup ((waybelow A1) /\ B1) by WAYBEL23:def 7
.= union ((waybelow A1) /\ B1) by A1, YELLOW_1:22 ;
then consider a being set such that
A4: p in a and
A5: a in (waybelow A1) /\ B1 by A3, TARSKI:def 4;
a in the carrier of L1 by A5;
then a in the topology of T by A1, YELLOW_1:1;
then reconsider a = a as Subset of T ;
take a ; :: thesis: ( a in B2 & p in a & a c= A )
thus a in B2 by A5, XBOOLE_0:def 4; :: thesis: ( p in a & a c= A )
thus p in a by A4; :: thesis: a c= A
reconsider a1 = a as Element of L1 by A5;
a1 in waybelow A1 by A5, XBOOLE_0:def 4;
then a1 << A1 by WAYBEL_3:7;
then a1 <= A1 by WAYBEL_3:1;
hence a c= A by A1, YELLOW_1:3; :: thesis: verum

end;

B2 c= the topology of T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B2 or x in the topology of T )
assume x in B2 ; :: thesis: x in the topology of T
then reconsider x1 = x as Element of L1 ;
x1 in the carrier of L1 ;
hence x in the topology of T by A1, YELLOW_1:1; :: thesis: verum

end;

hence B1 is Basis of T by A2, YELLOW_9:32; :: thesis: verum