let T be non empty TopSpace; :: thesis: for x being Point of T
for y being Point of TopStruct(# the carrier of T,the topology of T #)
for A being set st x = y holds
( A is Basis of x iff A is Basis of y )
let x be Point of T; :: thesis: for y being Point of TopStruct(# the carrier of T,the topology of T #)
for A being set st x = y holds
( A is Basis of x iff A is Basis of y )
let y be Point of TopStruct(# the carrier of T,the topology of T #); :: thesis: for A being set st x = y holds
( A is Basis of x iff A is Basis of y )
let A be set ; :: thesis: ( x = y implies ( A is Basis of x iff A is Basis of y ) )
assume Z:
x = y
; :: thesis: ( A is Basis of x iff A is Basis of y )
thus
( A is Basis of x implies A is Basis of y )
:: thesis: ( A is Basis of y implies A is Basis of x )proof
assume Z1:
A is
Basis of
x
;
:: thesis: A is Basis of y
then reconsider A =
A as
Subset-Family of
TopStruct(# the
carrier of
T,the
topology of
T #) ;
A is
Basis of
y
proof
thus
A c= the
topology of
TopStruct(# the
carrier of
T,the
topology of
T #)
by Z1, YELLOW_8:def 2;
:: according to YELLOW_8:def 2 :: thesis: ( y in Intersect A & ( for b1 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) holds
( not b1 is open or not y in b1 or ex b2 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) st
( b2 in A & b2 c= b1 ) ) ) )
thus
y in Intersect A
by Z, Z1, YELLOW_8:def 2;
:: thesis: for b1 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) holds
( not b1 is open or not y in b1 or ex b2 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) st
( b2 in A & b2 c= b1 ) )
let S be
Subset of
TopStruct(# the
carrier of
T,the
topology of
T #);
:: thesis: ( not S is open or not y in S or ex b1 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) st
( b1 in A & b1 c= S ) )
reconsider SS =
S as
Subset of
T ;
assume Z2:
(
S is
open &
y in S )
;
:: thesis: ex b1 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) st
( b1 in A & b1 c= S )
then
SS is
open
by PRE_TOPC:60;
then consider W being
Subset of
T such that W:
(
W in A &
W c= SS )
by Z2, Z, Z1, YELLOW_8:def 2;
reconsider V =
W as
Subset of
TopStruct(# the
carrier of
T,the
topology of
T #) ;
take
V
;
:: thesis: ( V in A & V c= S )
thus
(
V in A &
V c= S )
by W;
:: thesis: verum
end;
hence
A is
Basis of
y
;
:: thesis: verum
end;
assume Z1:
A is Basis of y
; :: thesis: A is Basis of x
then reconsider A = A as Subset-Family of T ;
A is Basis of x
hence
A is Basis of x
; :: thesis: verum