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

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 <> {} )
;

end;

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

hence PS is closed ; :: thesis: verum

end;

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 ` ) )

then
PS ` is open
by TOPS_1:25;( ( 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 ` )

( Q is open & Q c= PS ` & a in Q ) implies a in PS ` ) ; :: thesis: verum

end;( 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

thus
( ex Q being Subset of TS st
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;( 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

( Q is open & Q c= PS ` & a in Q ) implies a in PS ` ) ; :: thesis: verum

hence PS is closed ; :: thesis: verum