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 that
A1: the carrier of Y1 = MaxADSet A and
A2: the carrier of Y2 = MaxADSet A ; :: 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