let TS be TopSpace; :: thesis: for PS being Subset of TS st TS is Hausdorff & PS is compact holds
PS is closed
let PS be Subset of TS; :: thesis: ( TS is Hausdorff & PS is compact implies PS is closed )
assume that
A1: TS is Hausdorff and
A2: PS is compact ; :: thesis: PS is closed

per cases ( PS = {} or PS <> {} ) ;

suppose PS = {} ; :: thesis: PS is closed

hence PS is closed ; :: thesis: verum

end;

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

now

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

proof

assume A4: a in PS ` ; :: thesis: ex Q being Subset of TS st
( Q is open & Q c= PS ` & a in Q )
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, Th15;
W misses (V ` ) ` by A8;
then A9: ( W c= V ` & V ` c= PS ` ) by A7, SUBSET_1:31, SUBSET_1:44;
take Q = W; :: thesis: ( Q is open & Q c= PS ` & a in Q )
thus ( Q is open & Q c= PS ` & a in Q ) by A5, A6, A9, XBOOLE_1:1; :: thesis: verum

end;

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

end;

then PS ` is open by TOPS_1:57;
hence PS is closed by TOPS_1:29; :: thesis: verum

end;

end;