consider v being Element of X1;
v in X1 by A2;
then reconsider v = v as Element of X ;
v - v = 0. X by RLVECT_1:28;
hence 0. X is Element of X1 by A1, A2, CLVECT_1:23; :: thesis: verum