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