let X, Y be RealBanachSpace; :: thesis: for T being LinearOperator of X,Y st T is closed holds
graphNSP T is complete
let T be LinearOperator of X,Y; :: thesis: ( T is closed implies graphNSP T is complete )
graphNSP T is Subspace of [:X,Y:] by Th9;
hence ( T is closed implies graphNSP T is complete ) by Th10; :: thesis: verum