let X be TopSpace; :: thesis: for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is closed & C c= the carrier of X0 & A c= C & A = B holds
( B is closed iff A is closed )
let X0 be SubSpace of X; :: thesis: for C, A being Subset of X
for B being Subset of X0 st C is closed & C c= the carrier of X0 & A c= C & A = B holds
( B is closed iff A is closed )
let C, A be Subset of X; :: thesis: for B being Subset of X0 st C is closed & C c= the carrier of X0 & A c= C & A = B holds
( B is closed iff A is closed )
let B be Subset of X0; :: thesis: ( C is closed & C c= the carrier of X0 & A c= C & A = B implies ( B is closed iff A is closed ) )
assume that
A1: C is closed and
A2: C c= the carrier of X0 and
A3: A c= C and
A4: A = B ; :: thesis: ( B is closed iff A is closed )
thus ( B is closed implies A is closed ) :: thesis: ( A is closed implies B is closed )
proof
assume B is closed ; :: thesis: A is closed
then consider F being Subset of X such that
A5: F is closed and
A6: F /\ ([#] X0) = B by PRE_TOPC:13;
A c= F by A4, A6, XBOOLE_1:17;
then A7: A c= F /\ C by A3, XBOOLE_1:19;
F /\ C c= A by A2, A4, A6, XBOOLE_1:26;
hence A is closed by A1, A5, A7, XBOOLE_0:def 10; :: thesis: verum
end;
thus ( A is closed implies B is closed ) by A4, TOPS_2:26; :: thesis: verum