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

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