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 5
.= 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 5 ;
for C1 being Subset of
for C2 being Subset of st C1 = C2 holds
( C1 is open iff C2 is open )

proof

let C1 be Subset of ; :: thesis: for C2 being Subset of st C1 = C2 holds
( C1 is open iff C2 is open )
let C2 be Subset of ; :: 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 C1 is open ; :: thesis: C2 is open
then consider A being Subset-Family of such that
A3: C1 = union A and
A4: for e being set st e in A holds
ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:45;
reconsider AA = A as Subset-Family of by A1;
for e being set st e in AA holds
ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open )

proof

let e be set ; :: thesis: ( e in AA implies ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume e in AA ; :: thesis: ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then consider X1 being Subset of , Y1 being Subset of such that
A5: ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A4;
reconsider Y2 = Y1 as Subset of ;
reconsider X2 = X1 as Subset of ;
take X2 ; :: thesis: ex Y1 being Subset of 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;

hence C2 is open by A2, A3, BORSUK_1:45; :: thesis: verum

end;

assume C2 is open ; :: thesis: C1 is open
then consider A being Subset-Family of such that
A6: C2 = union A and
A7: for e being set st e in A holds
ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:45;
reconsider AA = A as Subset-Family of by A1;
for e being set st e in AA holds
ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open )

proof

let e be set ; :: thesis: ( e in AA implies ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume e in AA ; :: thesis: ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then consider X1 being Subset of , Y1 being Subset of such that
A8: ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A7;
reconsider Y2 = Y1 as Subset of ;
reconsider X2 = X1 as Subset of ;
take X2 ; :: thesis: ex Y1 being Subset of 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;

hence C1 is open by A2, A6, BORSUK_1:45; :: thesis: 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; :: thesis: verum