let T be TopStruct ; :: thesis: for Q being Subset of T
for A being SubSpace of T st Q is closed holds
for P being Subset of A st P = Q holds
P is closed
let Q be Subset of T; :: thesis: for A being SubSpace of T st Q is closed holds
for P being Subset of A st P = Q holds
P is closed
let A be SubSpace of T; :: thesis: ( Q is closed implies for P being Subset of A st P = Q holds
P is closed )
assume A1: Q is closed ; :: thesis: for P being Subset of A st P = Q holds
P is closed
let P be Subset of A; :: thesis: ( P = Q implies P is closed )
assume P = Q ; :: thesis: P is closed
then Q /\ ([#] A) = P by XBOOLE_1:28;
hence P is closed by A1, PRE_TOPC:13; :: thesis: verum