let T be non empty TopSpace; :: thesis: for x being Element of (InclPoset the topology of T)
for X being Subset of T st x = X holds
( x is compact iff X is compact )
let x be Element of (InclPoset the topology of T); :: thesis: for X being Subset of T st x = X holds
( x is compact iff X is compact )
let X be Subset of T; :: thesis: ( x = X implies ( x is compact iff X is compact ) )
assume A1: x = X ; :: thesis: ( x is compact iff X is compact )

hereby :: thesis: ( X is compact implies x is compact )

assume x is compact ; :: thesis: X is compact
then A2: x << x by Def2;
thus X is compact :: thesis: verum

proof

let F be Subset-Family of T; :: according to COMPTS_1:def 7 :: thesis: ( not F is Cover of X or not F is open or ex b₁ being Element of K10(K10(the carrier of T)) st
( b₁ c= F & b₁ is Cover of X & b₁ is finite ) )
assume that
A3: X c= union F and
A4: F is open ; :: according to SETFAM_1:def 12 :: thesis: ex b₁ being Element of K10(K10(the carrier of T)) st
( b₁ c= F & b₁ is Cover of X & b₁ is finite )
consider G being finite Subset of F such that
A5: x c= union G by A1, A2, A3, A4, Th34;
reconsider G = G as Subset-Family of T by XBOOLE_1:1;
take G ; :: thesis: ( G c= F & G is Cover of X & G is finite )
thus ( G c= F & X c= union G & G is finite ) by A1, A5; :: according to SETFAM_1:def 12 :: thesis: verum

end;

end;

assume A6: for F being Subset-Family of T st F is Cover of X & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of X & G is finite ) ; :: according to COMPTS_1:def 7 :: thesis: x is compact

now

let F be Subset-Family of T; :: thesis: ( F is open & x c= union F implies ex G being finite Subset of F st x c= union G )
assume A7: ( F is open & x c= union F ) ; :: thesis: ex G being finite Subset of F st x c= union G
F is Cover of X

proof

thus X c= union F by A1, A7; :: according to SETFAM_1:def 12 :: thesis: verum

end;

then consider G being Subset-Family of T such that
A8: ( G c= F & G is Cover of X & G is finite ) by A6, A7;
x c= union G by A1, A8, SETFAM_1:def 12;
hence ex G being finite Subset of F st x c= union G by A8; :: thesis: verum

end;

hence x << x by Th35; :: according to WAYBEL_3:def 2 :: thesis: verum