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 A3: X is Basis of l ; :: thesis: X is Basis of t
then A4: X c= the topology of L by TOPS_2:64;
A5: l in Intersect X by A3, YELLOW_8:def 1;
A6: 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 A3, YELLOW_8:def 1;
now :: thesis: for S being Subset of T st S is open & t in S holds
ex V being Subset of T st
( V in X9 & V c= S )
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
A7: S is open and
A8: 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 A7, PRE_TOPC:def 2;
then S9 is open by A1, PRE_TOPC:def 2;
then consider V being Subset of L such that
A9: ( V in X & V c= S9 ) by A2, A6, A8;
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 A9; :: thesis: verum
end;
hence X is Basis of t by A1, A2, A4, A5, TOPS_2:64, YELLOW_8:def 1; :: thesis: verum