now :: thesis: not Sspace A is proper

hence
not Sspace A is proper
; :: thesis: verumassume 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;the carrier of (Sspace A) = A by Lm3;

hence contradiction by A1, TEX_2:8; :: thesis: verum