let S, T be TopSpace; :: thesis: for A being closed Subset of S
for B being closed Subset of T holds [:A,B:] is closed
let A be closed Subset of S; :: thesis: for B being closed Subset of T holds [:A,B:] is closed
let B be closed Subset of T; :: thesis: [:A,B:] is closed
A1: ( Cl A = A & Cl B = B ) by PRE_TOPC:52;
Cl [:A,B:] = [:(Cl A),(Cl B):] by Th15;
hence [:A,B:] is closed by A1; :: thesis: verum