let S, T be non empty TopSpace; for G being Subset of [:S,T:] st ( for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) holds
G is open
let G be Subset of [:S,T:]; ( ( for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) implies G is open )
assume A1:
for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G )
; G is open
set A = { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } ;
{ [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } c= bool the carrier of [:S,T:]
proof
let e be
object ;
TARSKI:def 3 ( not e in { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } or e in bool the carrier of [:S,T:] )
assume
e in { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) }
;
e in bool the carrier of [:S,T:]
then
ex
GS being
Subset of
S ex
GT being
Subset of
T st
(
e = [:GS,GT:] &
GS is
open &
GT is
open &
[:GS,GT:] c= G )
;
hence
e in bool the
carrier of
[:S,T:]
;
verum
end;
then reconsider A = { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } as Subset-Family of [:S,T:] ;
reconsider A = A as Subset-Family of [:S,T:] ;
for x being object holds
( x in G iff ex Y being set st
( x in Y & Y in A ) )
proof
let x be
object ;
( x in G iff ex Y being set st
( x in Y & Y in A ) )
thus
(
x in G implies ex
Y being
set st
(
x in Y &
Y in A ) )
( ex Y being set st
( x in Y & Y in A ) implies x in G )proof
assume
x in G
;
ex Y being set st
( x in Y & Y in A )
then consider GS being
Subset of
S,
GT being
Subset of
T such that A2:
GS is
open
and A3:
GT is
open
and A4:
x in [:GS,GT:]
and A5:
[:GS,GT:] c= G
by A1;
take
[:GS,GT:]
;
( x in [:GS,GT:] & [:GS,GT:] in A )
thus
(
x in [:GS,GT:] &
[:GS,GT:] in A )
by A2, A3, A4, A5;
verum
end;
given Y being
set such that A6:
x in Y
and A7:
Y in A
;
x in G
ex
GS being
Subset of
S ex
GT being
Subset of
T st
(
Y = [:GS,GT:] &
GS is
open &
GT is
open &
[:GS,GT:] c= G )
by A7;
hence
x in G
by A6;
verum
end;
then A8:
G = union A
by TARSKI:def 4;
for e being set st e in A holds
ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
hence
G is open
by A8, BORSUK_1:5; verum