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

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