now :: thesis: not Sspace A is proper

assume A1: Sspace A is proper ; :: thesis: contradiction
the carrier of (Sspace A) = A by Lm3;
hence contradiction by A1, TEX_2:8; :: thesis: verum

end;

hence not Sspace A is proper ; :: thesis: verum