let X be TopSpace; :: thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is open SubSpace of X iff A is open )
let X0 be SubSpace of X; :: thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is open SubSpace of X iff A is open )
let A be Subset of X; :: thesis: ( A = the carrier of X0 implies ( X0 is open SubSpace of X iff A is open ) )
assume A1: A = the carrier of X0 ; :: thesis: ( X0 is open SubSpace of X iff A is open )
hence ( X0 is open SubSpace of X implies A is open ) by Def1; :: thesis: ( A is open implies X0 is open SubSpace of X )
thus ( A is open implies X0 is open SubSpace of X ) :: thesis: verum
proof
assume A is open ; :: thesis: X0 is open SubSpace of X
then for B being Subset of X st B = the carrier of X0 holds
B is open by A1;
hence X0 is open SubSpace of X by Def1; :: thesis: verum
end;