let S1, S2, T1, T2 be non empty TopSpace; :: thesis: for f being continuous Function of S1,T1
for g being continuous Function of S2,T2
for P2 being Subset of [:T1,T2:] st P2 is open holds
[:f,g:] " P2 is open
let f be continuous Function of S1,T1; :: thesis: for g being continuous Function of S2,T2
for P2 being Subset of [:T1,T2:] st P2 is open holds
[:f,g:] " P2 is open
let g be continuous Function of S2,T2; :: thesis: for P2 being Subset of [:T1,T2:] st P2 is open holds
[:f,g:] " P2 is open
let P2 be Subset of [:T1,T2:]; :: thesis: ( P2 is open implies [:f,g:] " P2 is open )
reconsider Kill = [:f,g:] " (Base-Appr P2) as Subset-Family of [:S1,S2:] ;
for P being Subset of [:S1,S2:] st P in Kill holds
P is open

proof

let P be Subset of [:S1,S2:]; :: thesis: ( P in Kill implies P is open )
assume P in Kill ; :: thesis: P is open
then ex B being Subset of [:T1,T2:] st
( B in Base-Appr P2 & P = [:f,g:] " B ) by FUNCT_2:def 9;
hence P is open by Th8; :: thesis: verum

end;

then A1: Kill is open by TOPS_2:def 1;
assume P2 is open ; :: thesis: [:f,g:] " P2 is open
then P2 = union (Base-Appr P2) by BORSUK_1:13;
then [:f,g:] " P2 = union ([:f,g:] " (Base-Appr P2)) by Th7;
hence [:f,g:] " P2 is open by A1, TOPS_2:19; :: thesis: verum