reconsider A = the carrier of x as Subset of VS by VECTSP_4:def 2;

consider X being Subspace of VS such that

A1: X = x ;

take A ; :: thesis: ex X being Subspace of VS st

( x = X & A = the carrier of X )

take X ; :: thesis: ( x = X & A = the carrier of X )

thus ( x = X & A = the carrier of X ) by A1; :: thesis: verum

consider X being Subspace of VS such that

A1: X = x ;

take A ; :: thesis: ex X being Subspace of VS st

( x = X & A = the carrier of X )

take X ; :: thesis: ( x = X & A = the carrier of X )

thus ( x = X & A = the carrier of X ) by A1; :: thesis: verum