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 ;
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 ;
then consider b being set such that
A8: x in b and
A9: b in Z by ;
A10: x in Y by ;
A11: Y c= b
proof
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 ;
A14: i in dom (MergeSequence (p,q)) by ;
now :: thesis: (MergeSequence (p,q)) . i = b
per cases ( q . i = TRUE or q . i = FALSE ) by XBOOLEAN:def 3;
suppose q . i = TRUE ; :: thesis: (MergeSequence (p,q)) . i = b
hence (MergeSequence (p,q)) . i = b by ; :: thesis: verum
end;
suppose q . i = FALSE ; :: thesis: (MergeSequence (p,q)) . i = b
then A15: (MergeSequence (p,q)) . i = the carrier of T \ b by ;
(MergeSequence (p,q)) . i in rng (MergeSequence (p,q)) by ;
then Y c= the carrier of T \ b by ;
hence (MergeSequence (p,q)) . i = b by ; :: thesis: verum
end;
end;
end;
then A16: b in rng (MergeSequence (p,q)) by ;
assume z in Y ; :: thesis: z in b
hence z in b by ; :: thesis: verum
end;
b c= X by ;
hence Y c= X by A11; :: thesis: verum