let Y1, Y2 be strict SubSpace of Y; :: thesis: ( the carrier of Y1 = MaxADSet A & the carrier of Y2 = MaxADSet A implies Y1 = Y2 )
assume A1: ( the carrier of Y1 = MaxADSet A & the carrier of Y2 = MaxADSet A ) ; :: thesis: Y1 = Y2
set A1 = the carrier of Y1;
set A2 = the carrier of Y2;
A2: ( the carrier of Y1 = [#] Y1 & the carrier of Y2 = [#] Y2 ) ;
then ( the carrier of Y1 c= [#] Y & the carrier of Y2 c= [#] Y ) by PRE_TOPC:def 9;
then reconsider A1 = the carrier of Y1, A2 = the carrier of Y2 as Subset of Y ;
( Y1 = Y | A1 & Y2 = Y | A2 ) by A2, PRE_TOPC:def 10;
hence Y1 = Y2 by A1; :: thesis: verum