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 A1: 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 )
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 A2: B is Basis of T ; :: thesis: for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
let Y be set ; :: thesis: ( not Y in Components B or X misses Y or Y c= X )
assume A3: Y in Components B ; :: thesis: ( X misses Y or Y c= X )
assume X /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: Y c= X
then consider x being set such that
A4: x in X /\ Y by XBOOLE_0:def 1;
A5: ( x in X & x in Y ) by A4, XBOOLE_0:def 4;
consider p being FinSequence of bool the carrier of T such that
len p = card B and
A6: rng p = B and
A7: Components B = { (Intersect (rng (MergeSequence p,q))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;
A8: X in the topology of T by A1, PRE_TOPC:def 5;
the topology of T c= UniCl B by A2, CANTOR_1:def 2;
then consider Z being Subset-Family of T such that
A9: Z c= B and
A10: X = union Z by A8, CANTOR_1:def 1;
consider b being set such that
A11: x in b and
A12: b in Z by A5, A10, TARSKI:def 4;
A13: b c= X by A10, A12, ZFMISC_1:92;
consider q being FinSequence of BOOLEAN such that
A14: Y = Intersect (rng (MergeSequence p,q)) and
len q = len p by A3, A7;
Y c= b

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Y or z in b )
assume A15: z in Y ; :: thesis: z in b
consider i being Nat such that
A16: i in dom p and
A17: p . i = b by A6, A9, A12, FINSEQ_2:11;
A18: i in dom (MergeSequence p,q) by A16, Th5;

now

per cases ( q . i = TRUE or not q . i = TRUE ) ;

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

hence (MergeSequence p,q) . i = b by A17, Th6; :: thesis: verum

end;

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

then q . i = FALSE by XBOOLEAN:def 3;
then A19: (MergeSequence p,q) . i = the carrier of T \ b by A16, A17, Th7;
(MergeSequence p,q) . i in rng (MergeSequence p,q) by A18, FUNCT_1:def 5;
then Y c= the carrier of T \ b by A14, A19, MSSUBFAM:2;
hence (MergeSequence p,q) . i = b by A5, A11, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

then b in rng (MergeSequence p,q) by A18, FUNCT_1:def 5;
hence z in b by A14, A15, SETFAM_1:58; :: thesis: verum

end;

hence Y c= X by A13, XBOOLE_1:1; :: thesis: verum