let T be TopStruct ; :: thesis: for A being SubSpace of T
for Q being Subset of T st Q c= [#] A holds
( Q is compact iff for P being Subset of A st P = Q holds
P is compact )
let A be SubSpace of T; :: thesis: for Q being Subset of T st Q c= [#] A holds
( Q is compact iff for P being Subset of A st P = Q holds
P is compact )
let Q be Subset of T; :: thesis: ( Q c= [#] A implies ( Q is compact iff for P being Subset of A st P = Q holds
P is compact ) )
[#] A c= [#] T by PRE_TOPC:def 4;
then reconsider AA = [#] A as Subset of T ;
assume A1: Q c= [#] A ; :: thesis: ( Q is compact iff for P being Subset of A st P = Q holds
P is compact )
then A2: Q /\ AA = Q by XBOOLE_1:28;
thus ( Q is compact implies for P being Subset of A st P = Q holds
P is compact ) :: thesis: ( ( for P being Subset of A st P = Q holds
P is compact ) implies Q is compact )

proof

assume A3: Q is compact ; :: thesis: for P being Subset of A st P = Q holds
P is compact
let P be Subset of A; :: thesis: ( P = Q implies P is compact )
assume A4: P = Q ; :: thesis: P is compact
thus P is compact :: thesis: verum

proof

let G be Subset-Family of A; :: according to COMPTS_1:def 4 :: thesis: ( G is Cover of P & G is open implies ex G being Subset-Family of A st
( G c= G & G is Cover of P & G is finite ) )
set GG = G;
assume that
A5: G is Cover of P and
A6: G is open ; :: thesis: ex G being Subset-Family of A st
( G c= G & G is Cover of P & G is finite )
consider F being Subset-Family of T such that
A7: F is open and
A8: for AA being Subset of T st AA = [#] A holds
G = F | AA by A6, TOPS_2:39;
A9: Q c= union G by A4, A5, SETFAM_1:def 11;
union (F | AA) c= union F by TOPS_2:34;
then union G c= union F by A8;
then Q c= union F by A9;
then F is Cover of Q by SETFAM_1:def 11;
then consider F9 being Subset-Family of T such that
A10: F9 c= F and
A11: F9 is Cover of Q and
A12: F9 is finite by A3, A7;
F9 | AA c= bool ([#] (T | AA)) ;
then reconsider G9 = F9 | AA as Subset-Family of A by PRE_TOPC:def 5;
take G9 ; :: thesis: ( G9 c= G & G9 is Cover of P & G9 is finite )
F9 | AA c= F | AA by A10, TOPS_2:30;
hence G9 c= G by A8; :: thesis: ( G9 is Cover of P & G9 is finite )
Q c= union F9 by A11, SETFAM_1:def 11;
then P c= union G9 by A2, A4, TOPS_2:32;
hence G9 is Cover of P by SETFAM_1:def 11; :: thesis: G9 is finite
thus G9 is finite by A12, TOPS_2:36; :: thesis: verum

end;

end;

thus ( ( for P being Subset of A st P = Q holds
P is compact ) implies Q is compact ) :: thesis: verum

proof

reconsider QQ = Q as Subset of A by A1;
assume for P being Subset of A st P = Q holds
P is compact ; :: thesis: Q is compact
then A13: QQ is compact ;
thus Q is compact :: thesis: verum

proof

let F be Subset-Family of T; :: according to COMPTS_1:def 4 :: thesis: ( F is Cover of Q & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of Q & G is finite ) )
set F9 = F;
assume that
A14: F is Cover of Q and
A15: F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of Q & G is finite )
consider f being Function such that
A16: dom f = F and
A17: rng f = F | AA and
A18: for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ AA by TOPS_2:40;
F | AA c= bool ([#] (T | AA)) ;
then reconsider F9 = rng f as Subset-Family of A by A17, PRE_TOPC:def 5;
A19: F9 is open

proof

let X be Subset of A; :: according to TOPS_2:def 1 :: thesis: ( not X in F9 or X is open )
assume A20: X in F9 ; :: thesis: X is open
then reconsider Y = X as Subset of (T | AA) by A17;
consider R being Subset of T such that
A21: R in F and
A22: R /\ AA = Y by A17, A20, TOPS_2:def 3;
R is open by A15, A21;
then R in the topology of T ;
then X in the topology of A by A22, PRE_TOPC:def 4;
hence X is open ; :: thesis: verum

end;

Q c= union F by A14, SETFAM_1:def 11;
then QQ c= union F9 by A2, A17, TOPS_2:32;
then F9 is Cover of QQ by SETFAM_1:def 11;
then consider G being Subset-Family of A such that
A23: G c= F9 and
A24: G is Cover of QQ and
A25: G is finite by A13, A19;
consider X being set such that
A26: X c= dom f and
A27: X is finite and
A28: f .: X = G by A23, A25, ORDERS_1:85;
reconsider G9 = X as Subset-Family of T by A16, A26, TOPS_2:2;
take G9 ; :: thesis: ( G9 c= F & G9 is Cover of Q & G9 is finite )
Q c= union G9

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in union G9 )
assume A29: x in Q ; :: thesis: x in union G9
QQ c= union G by A24, SETFAM_1:def 11;
then consider Y being set such that
A30: x in Y and
A31: Y in G by A29, TARSKI:def 4;
consider z being object such that
A32: z in dom f and
A33: z in X and
A34: f . z = Y by A28, A31, FUNCT_1:def 6;
reconsider Z = z as Subset of T by A16, A32;
Y = Z /\ AA by A16, A18, A32, A34;
then x in Z by A30, XBOOLE_0:def 4;
hence x in union G9 by A33, TARSKI:def 4; :: thesis: verum

end;

hence ( G9 c= F & G9 is Cover of Q & G9 is finite ) by A16, A26, A27, SETFAM_1:def 11; :: thesis: verum

end;

end;