let S, T be TopSpace; TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
A1: the carrier of [:S,T:] =
[: the carrier of S, the carrier of T:]
by BORSUK_1:def 2
.=
the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
by BORSUK_1:def 2
;
for C1 being Subset of [:S,T:]
for C2 being Subset of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] st C1 = C2 holds
( C1 is open iff C2 is open )
proof
let C1 be
Subset of
[:S,T:];
for C2 being Subset of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] st C1 = C2 holds
( C1 is open iff C2 is open )let C2 be
Subset of
[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):];
( C1 = C2 implies ( C1 is open iff C2 is open ) )
assume A2:
C1 = C2
;
( C1 is open iff C2 is open )
hereby ( C2 is open implies C1 is open )
assume
C1 is
open
;
C2 is open then consider A being
Subset-Family of
[:S,T:] such that A3:
C1 = union A
and A4:
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 )
by BORSUK_1:5;
reconsider AA =
A as
Subset-Family of
[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] by A1;
for
e being
set st
e in AA holds
ex
X1 being
Subset of
TopStruct(# the
carrier of
S, the
topology of
S #) ex
Y1 being
Subset of
TopStruct(# the
carrier of
T, the
topology of
T #) st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
proof
let e be
set ;
( e in AA implies ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume
e in AA
;
ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then consider X1 being
Subset of
S,
Y1 being
Subset of
T such that A5:
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
by A4;
reconsider Y2 =
Y1 as
Subset of
TopStruct(# the
carrier of
T, the
topology of
T #) ;
reconsider X2 =
X1 as
Subset of
TopStruct(# the
carrier of
S, the
topology of
S #) ;
take
X2
;
ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X2,Y1:] & X2 is open & Y1 is open )
take
Y2
;
( e = [:X2,Y2:] & X2 is open & Y2 is open )
thus
(
e = [:X2,Y2:] &
X2 is
open &
Y2 is
open )
by A5, TOPS_3:76;
verum
end; hence
C2 is
open
by A2, A3, BORSUK_1:5;
verum
end;
assume
C2 is
open
;
C1 is open
then consider A being
Subset-Family of
[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] such that A6:
C2 = union A
and A7:
for
e being
set st
e in A holds
ex
X1 being
Subset of
TopStruct(# the
carrier of
S, the
topology of
S #) ex
Y1 being
Subset of
TopStruct(# the
carrier of
T, the
topology of
T #) st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
by BORSUK_1:5;
reconsider AA =
A as
Subset-Family of
[:S,T:] by A1;
for
e being
set st
e in AA holds
ex
X1 being
Subset of
S ex
Y1 being
Subset of
T st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
proof
let e be
set ;
( e in AA implies ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume
e in AA
;
ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then consider X1 being
Subset of
TopStruct(# the
carrier of
S, the
topology of
S #),
Y1 being
Subset of
TopStruct(# the
carrier of
T, the
topology of
T #)
such that A8:
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
by A7;
reconsider Y2 =
Y1 as
Subset of
T ;
reconsider X2 =
X1 as
Subset of
S ;
take
X2
;
ex Y1 being Subset of T st
( e = [:X2,Y1:] & X2 is open & Y1 is open )
take
Y2
;
( e = [:X2,Y2:] & X2 is open & Y2 is open )
thus
(
e = [:X2,Y2:] &
X2 is
open &
Y2 is
open )
by A8, TOPS_3:76;
verum
end;
hence
C1 is
open
by A2, A6, BORSUK_1:5;
verum
end;
hence
TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
by A1, TOPS_3:72; verum