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