let TS be TopSpace; :: thesis: for PS being Subset of TS st TS is T_2 & PS is compact holds
PS is closed
let PS be Subset of TS; :: thesis: ( TS is T_2 & PS is compact implies PS is closed )
assume that
A1: TS is T_2 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 :: thesis: for a being set holds
( ( 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 ` ) )

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, Th6;
take Q = W; :: thesis: ( Q is open & Q c= PS ` & a in Q )
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: 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:25;
hence PS is closed ; :: thesis: verum

end;

end;