let TS be TopSpace; :: thesis:
let PS be Subset of TS; :: thesis:
assume that
A1: TS is T_2 and
A2: PS is compact ; :: thesis:

per cases ;

suppose PS = {} ; :: thesis:

hence PS is closed ; :: thesis:

end;

suppose A3: PS <> {} ; :: thesis:

now :: thesis:

let a be set ; :: thesis:
thus ( a in PS ` implies ex Q being Subset of TS st
( Q is open & Q c= PS ` & a in Q ) ) :: thesis:

proof

assume A4: a in PS ` ; :: thesis:
then reconsider p = a as Point of TS ;
consider W, V being Subset of TS such that
A5: W is open and
V is open and
A6: p in W and
A7: PS c= V and
A8: W misses V by A1, A2, A3, A4, Th6;
take Q = W; :: thesis:
W misses (V `) ` by A8;
then A9: W c= V ` by SUBSET_1:24;
V ` c= PS ` by A7, SUBSET_1:12;
hence ( Q is open & Q c= PS ` & a in Q ) by A5, A6, A9; :: thesis:

end;

thus ( ex Q being Subset of TS st
( Q is open & Q c= PS ` & a in Q ) implies a in PS ` ) ; :: thesis:

end;

then PS ` is open by TOPS_1:25;
hence PS is closed ; :: thesis:

end;

end;