let T be TopSpace; for U, V being Subset of T
for B being set st U in B & V in B & B \/ {(U \/ V)} is Basis of T holds
B is Basis of T
let U, V be Subset of T; for B being set st U in B & V in B & B \/ {(U \/ V)} is Basis of T holds
B is Basis of T
let B be set ; ( U in B & V in B & B \/ {(U \/ V)} is Basis of T implies B is Basis of T )
assume that
A1:
U in B
and
A2:
V in B
and
A3:
B \/ {(U \/ V)} is Basis of T
; B is Basis of T
A4:
B c= B \/ {(U \/ V)}
by XBOOLE_1:7;
then reconsider B9 = B as Subset-Family of T by A3, XBOOLE_1:1;
A5:
now for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B9 & p in a & a c= A )A6:
V c= U \/ V
by XBOOLE_1:7;
A7:
U c= U \/ V
by XBOOLE_1:7;
let A be
Subset of
T;
( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in B9 & p in a & a c= A ) )assume A8:
A is
open
;
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B9 & p in a & a c= A )let p be
Point of
T;
( p in A implies ex a being Subset of T st
( a in B9 & p in a & a c= A ) )assume
p in A
;
ex a being Subset of T st
( a in B9 & p in a & a c= A )then consider A9 being
Subset of
T such that A9:
A9 in B \/ {(U \/ V)}
and A10:
p in A9
and A11:
A9 c= A
by A3, A8, YELLOW_9:31;
assume A12:
for
a being
Subset of
T holds
( not
a in B9 or not
p in a or not
a c= A )
;
contradiction
(
A9 in B or
A9 = U \/ V )
by A9, ZFMISC_1:136;
then
( (
p in U &
U c= A ) or (
p in V &
V c= A ) )
by A10, A11, A12, A7, A6, XBOOLE_0:def 3;
hence
contradiction
by A1, A2, A12;
verum end;
B \/ {(U \/ V)} c= the topology of T
by A3, TOPS_2:64;
hence
B is Basis of T
by A5, A4, XBOOLE_1:1, YELLOW_9:32; verum