let Y1, Y2 be non empty strict SubSpace of Y; :: thesis: ( the carrier of Y1 = {y} & the carrier of Y2 = {y} implies Y1 = Y2 )
assume that
A1: the carrier of Y1 = {y} and
A2: the carrier of Y2 = {y} ; :: thesis: Y1 = Y2
set A1 = the carrier of Y1;
set A2 = the carrier of Y2;
A3: the carrier of Y2 = [#] Y2 ;
A4: the carrier of Y1 = [#] Y1 ;
then the carrier of Y1 c= [#] Y by PRE_TOPC:def 4;
then reconsider A1 = the carrier of Y1 as Subset of Y ;
Y1 = Y | A1 by A4, PRE_TOPC:def 5;
hence Y1 = Y2 by A1, A2, A3, PRE_TOPC:def 5; :: thesis: verum