let S, T be TopSpace; :: thesis: 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 )

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

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; :: thesis: verum
let C1 be Subset of [:S,T:]; :: thesis: 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 #):]; :: thesis: ( C1 = C2 implies ( C1 is open iff C2 is open ) )

assume A2: C1 = C2 ; :: thesis: ( C1 is open iff C2 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 )

end;( 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 #):]; :: thesis: ( C1 = C2 implies ( C1 is open iff C2 is open ) )

assume A2: C1 = C2 ; :: thesis: ( C1 is open iff C2 is open )

hereby :: thesis: ( C2 is open implies C1 is open )

assume
C2 is open
; :: thesis: C1 is open assume
C1 is open
; :: thesis: 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 )

end;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

hence
C2 is open
by A2, A3, BORSUK_1:5; :: thesis: verum
let e be set ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( e = [:X2,Y2:] & X2 is open & Y2 is open )

thus ( e = [:X2,Y2:] & X2 is open & Y2 is open ) by A5, TOPS_3:76; :: thesis: verum

end;( e = [:X1,Y1:] & X1 is open & Y1 is open ) )

assume e in AA ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( e = [:X2,Y2:] & X2 is open & Y2 is open )

thus ( e = [:X2,Y2:] & X2 is open & Y2 is open ) by A5, TOPS_3:76; :: thesis: verum

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

hence
C1 is open
by A2, A6, BORSUK_1:5; :: thesis: verum
let e be set ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex Y1 being Subset of T st

( e = [:X2,Y1:] & X2 is open & Y1 is open )

take Y2 ; :: thesis: ( e = [:X2,Y2:] & X2 is open & Y2 is open )

thus ( e = [:X2,Y2:] & X2 is open & Y2 is open ) by A8, TOPS_3:76; :: thesis: verum

end;( e = [:X1,Y1:] & X1 is open & Y1 is open ) )

assume e in AA ; :: thesis: 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 ; :: thesis: ex Y1 being Subset of T st

( e = [:X2,Y1:] & X2 is open & Y1 is open )

take Y2 ; :: thesis: ( e = [:X2,Y2:] & X2 is open & Y2 is open )

thus ( e = [:X2,Y2:] & X2 is open & Y2 is open ) by A8, TOPS_3:76; :: thesis: verum