let TS be TopSpace; :: thesis: for PS, QS being Subset of TS st PS is compact & QS c= PS & QS is closed holds
QS is compact
let PS, QS be Subset of TS; :: thesis: ( PS is compact & QS c= PS & QS is closed implies QS is compact )
assume that
A1: PS is compact and
A2: QS c= PS and
A3: QS is closed ; :: thesis: QS is compact
per cases ( PS = {} or PS <> {} ) ;
suppose PS = {} ; :: thesis: QS is compact
hence QS is compact by A2; :: thesis: verum
end;
suppose PS <> {} ; :: thesis: QS is compact
then TS | PS is compact by A1, Th3;
then A4: for QQ being Subset of (TS | PS) st QQ = QS holds
QQ is compact by A3, Th8, TOPS_2:26;
PS = [#] (TS | PS) by PRE_TOPC:def 5;
hence QS is compact by A2, A4, Th2; :: thesis: verum
end;
end;