let T be TopStruct ; for X being Subset of T st X is open holds
for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
let X be Subset of T; ( X is open implies for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X ) )
assume
X is open
; for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
then A1:
X in the topology of T
by PRE_TOPC:def 2;
let B be finite Subset-Family of T; ( B is Basis of T implies for Y being set holds
( not Y in Components B or X misses Y or Y c= X ) )
assume
B is Basis of T
; for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
then
the topology of T c= UniCl B
by CANTOR_1:def 2;
then consider Z being Subset-Family of T such that
A2:
Z c= B
and
A3:
X = union Z
by A1, CANTOR_1:def 1;
let Y be set ; ( not Y in Components B or X misses Y or Y c= X )
consider p being FinSequence of bool the carrier of T such that
len p = card B
and
A4:
rng p = B
and
A5:
Components B = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p }
by Def2;
assume
Y in Components B
; ( X misses Y or Y c= X )
then consider q being FinSequence of BOOLEAN such that
A6:
Y = Intersect (rng (MergeSequence (p,q)))
and
len q = len p
by A5;
assume
X /\ Y <> {}
; XBOOLE_0:def 7 Y c= X
then consider x being object such that
A7:
x in X /\ Y
by XBOOLE_0:def 1;
x in X
by A7, XBOOLE_0:def 4;
then consider b being set such that
A8:
x in b
and
A9:
b in Z
by A3, TARSKI:def 4;
A10:
x in Y
by A7, XBOOLE_0:def 4;
A11:
Y c= b
proof
let z be
object ;
TARSKI:def 3 ( not z in Y or z in b )
consider i being
Nat such that A12:
i in dom p
and A13:
p . i = b
by A4, A2, A9, FINSEQ_2:10;
A14:
i in dom (MergeSequence (p,q))
by A12, Th1;
now (MergeSequence (p,q)) . i = bper cases
( q . i = TRUE or q . i = FALSE )
by XBOOLEAN:def 3;
suppose
q . i = FALSE
;
(MergeSequence (p,q)) . i = bthen A15:
(MergeSequence (p,q)) . i = the
carrier of
T \ b
by A12, A13, Th3;
(MergeSequence (p,q)) . i in rng (MergeSequence (p,q))
by A14, FUNCT_1:def 3;
then
Y c= the
carrier of
T \ b
by A6, A15, MSSUBFAM:2;
hence
(MergeSequence (p,q)) . i = b
by A10, A8, XBOOLE_0:def 5;
verum end;
then A16:
b in rng (MergeSequence (p,q))
by A14, FUNCT_1:def 3;
assume
z in Y
;
z in b
hence
z in b
by A6, A16, SETFAM_1:43;
verum
end;
b c= X
by A3, A9, ZFMISC_1:74;
hence
Y c= X
by A11; verum