let TS be TopSpace; :: thesis: for PS, QS being Subset of TS st TS is T_2 & PS is compact & QS is compact holds

PS /\ QS is compact

let PS, QS be Subset of TS; :: thesis: ( TS is T_2 & PS is compact & QS is compact implies PS /\ QS is compact )

assume that

A1: TS is T_2 and

A2: PS is compact and

A3: QS is compact ; :: thesis: PS /\ QS is compact

A4: QS is closed by A1, A3, Th7;

PS is closed by A1, A2, Th7;

hence PS /\ QS is compact by A2, A4, Th9, XBOOLE_1:17; :: thesis: verum

PS /\ QS is compact

let PS, QS be Subset of TS; :: thesis: ( TS is T_2 & PS is compact & QS is compact implies PS /\ QS is compact )

assume that

A1: TS is T_2 and

A2: PS is compact and

A3: QS is compact ; :: thesis: PS /\ QS is compact

A4: QS is closed by A1, A3, Th7;

PS is closed by A1, A2, Th7;

hence PS /\ QS is compact by A2, A4, Th9, XBOOLE_1:17; :: thesis: verum