let T be TopStruct ; :: thesis:
let A be SubSpace of T; :: thesis:
let Q be Subset of T; :: thesis:
[#] A c= [#] T by PRE_TOPC:def 9;
then reconsider AA = [#] A as Subset of T ;
assume A1: Q c= [#] A ; :: thesis:
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:

assume A3: Q is compact ; :: thesis:
let P be Subset of A; :: thesis:
assume A4: P = Q ; :: thesis:
thus P is compact :: thesis:

let G be Subset-Family of A; :: according to COMPTS_1:def 7 :: thesis:
set GG = G;
assume that
A5: G is Cover of P and
A6: G is open ; :: thesis:
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:49;
A9: Q c= union G by A4, A5, SETFAM_1:def 12;
union (F | AA) c= union F by TOPS_2:44;
then union G c= union F by A8;
then Q c= union F by A9, XBOOLE_1:1;
then F is Cover of Q by SETFAM_1:def 12;
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, Def7;
F9 | AA c= bool ([#] (T | AA)) ;
then reconsider G9 = F9 | AA as Subset-Family of A by PRE_TOPC:def 10;
take G9 ; :: thesis:
F9 | AA c= F | AA by A10, TOPS_2:40;
hence G9 c= G by A8; :: thesis:
Q c= union F9 by A11, SETFAM_1:def 12;
then P c= union G9 by A2, A4, TOPS_2:42;
hence G9 is Cover of P by SETFAM_1:def 12; :: thesis:
thus G9 is finite by A12, TOPS_2:46; :: thesis:

end;

end;

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

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

let F be Subset-Family of T; :: according to COMPTS_1:def 7 :: thesis:
set F9 = F;
assume that
A14: F is Cover of Q and
A15: F is open ; :: thesis:
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:50;
F | AA c= bool ([#] (T | AA)) ;
then reconsider F9 = rng f as Subset-Family of A by A17, PRE_TOPC:def 10;
A19: F9 is open

let X be Subset of A; :: according to TOPS_2:def 1 :: thesis:
assume A20: X in F9 ; :: thesis:
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, TOPS_2:def 1;
then R in the topology of T by PRE_TOPC:def 5;
then X in the topology of A by A22, PRE_TOPC:def 9;
hence X is open by PRE_TOPC:def 5; :: thesis:

end;

Q c= union F by A14, SETFAM_1:def 12;
then QQ c= union F9 by A2, A17, TOPS_2:42;
then F9 is Cover of QQ by SETFAM_1:def 12;
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, Def7;
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:195;
reconsider G9 = X as Subset-Family of T by A16, A26, TOPS_2:3;
take G9 ; :: thesis:
Q c= union G9

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A29: x in Q ; :: thesis:
QQ c= union G by A24, SETFAM_1:def 12;
then consider Y being set such that
A30: x in Y and
A31: Y in G by A29, TARSKI:def 4;
consider z being set such that
A32: z in dom f and
A33: z in X and
A34: f . z = Y by A28, A31, FUNCT_1:def 12;
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:

end;

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

end;

end;