let M be non empty MetrSpace; :: thesis: for S being non empty Subset of M holds
( ( M | S is totally_bounded & M | S is complete ) iff S is sequentially_compact )
let S be non empty Subset of M; :: thesis: ( ( M | S is totally_bounded & M | S is complete ) iff S is sequentially_compact )
hereby :: thesis: ( S is sequentially_compact implies ( M | S is totally_bounded & M | S is complete ) )
assume ( M | S is totally_bounded & M | S is complete ) ; :: thesis: S is sequentially_compact
then M | S is sequentially_compact by Th12;
hence S is sequentially_compact by Th14; :: thesis: verum
end;
assume S is sequentially_compact ; :: thesis: ( M | S is totally_bounded & M | S is complete )
then M | S is sequentially_compact by Th14;
hence ( M | S is totally_bounded & M | S is complete ) by Th12; :: thesis: verum