let T be TopStruct ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: 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

hence Y c= X by A11; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: 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

b c= X
by A3, A9, ZFMISC_1:74;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( 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;

assume z in Y ; :: thesis: z in b

hence z in b by A6, A16, SETFAM_1:43; :: thesis: verum

end;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 :: thesis: (MergeSequence (p,q)) . i = bend;

then A16:
b in rng (MergeSequence (p,q))
by A14, FUNCT_1:def 3;per cases
( q . i = TRUE or q . i = FALSE )
by XBOOLEAN:def 3;

end;

suppose
q . i = FALSE
; :: thesis: (MergeSequence (p,q)) . i = b

then 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; :: thesis: verum

end;(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; :: thesis: verum

assume z in Y ; :: thesis: z in b

hence z in b by A6, A16, SETFAM_1:43; :: thesis: verum

hence Y c= X by A11; :: thesis: verum