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

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