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
( Cl A = A & Cl [:A,B:] = [:(Cl A),(Cl B):] ) by Th14, PRE_TOPC:22;
hence [:A,B:] is closed by PRE_TOPC:22; :: thesis: verum