let T be non empty TopSpace; :: thesis: for L being TopLattice
for t being Point of T
for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of L,the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let L be TopLattice; :: thesis: for t being Point of T
for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of L,the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let t be Point of T; :: thesis: for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of L,the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let l be Point of L; :: thesis: for X being Subset-Family of L st TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of L,the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let X be Subset-Family of L; :: thesis: ( TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of L,the topology of L #) & t = l & X is Basis of l implies X is Basis of t )
assume A1: TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of L,the topology of L #) ; :: thesis: ( not t = l or not X is Basis of l or X is Basis of t )
then reconsider X9 = X as Subset-Family of T ;
assume A2: t = l ; :: thesis: ( not X is Basis of l or X is Basis of t )
assume A0: X is Basis of l ; :: thesis: X is Basis of t
then A3: X c= the topology of L by TOPS_2:78;
A4: l in Intersect X by A0, YELLOW_8:def 2;
A5: for S being Subset of L st S is open & l in S holds
ex V being Subset of L st
( V in X & V c= S ) by A0, YELLOW_8:def 2;

now

let S be Subset of T; :: thesis: ( S is open & t in S implies ex V being Subset of T st
( V in X9 & V c= S ) )
assume that
A6: S is open and
A7: t in S ; :: thesis: ex V being Subset of T st
( V in X9 & V c= S )
reconsider S9 = S as Subset of L by A1;
S in the topology of T by A6, PRE_TOPC:def 5;
then S9 is open by A1, PRE_TOPC:def 5;
then consider V being Subset of L such that
A8: ( V in X & V c= S9 ) by A2, A5, A7;
reconsider V = V as Subset of T by A1;
take V = V; :: thesis: ( V in X9 & V c= S )
thus ( V in X9 & V c= S ) by A8; :: thesis: verum

end;

hence X is Basis of t by A1, A2, A3, A4, YELLOW_8:def 2, TOPS_2:78; :: thesis: verum