let Y be non empty TopStruct ; :: thesis: for Y0 being non empty SubSpace of Y

for Y1 being non empty V144() SubSpace of Y st Y0 is SubSpace of Y1 holds

Y0 is V144()

let Y0 be non empty SubSpace of Y; :: thesis: for Y1 being non empty V144() SubSpace of Y st Y0 is SubSpace of Y1 holds

Y0 is V144()

let Y1 be non empty V144() SubSpace of Y; :: thesis: ( Y0 is SubSpace of Y1 implies Y0 is V144() )

reconsider A1 = the carrier of Y1, A0 = the carrier of Y0 as non empty Subset of Y by Lm3;

assume A1: Y0 is SubSpace of Y1 ; :: thesis: Y0 is V144()

A2: A1 is T_0 by Th13;

( [#] Y0 = A0 & [#] Y1 = A1 ) ;

then A0 c= A1 by A1, PRE_TOPC:def 4;

then A0 is T_0 by A2;

hence Y0 is V144() ; :: thesis: verum

for Y1 being non empty V144() SubSpace of Y st Y0 is SubSpace of Y1 holds

Y0 is V144()

let Y0 be non empty SubSpace of Y; :: thesis: for Y1 being non empty V144() SubSpace of Y st Y0 is SubSpace of Y1 holds

Y0 is V144()

let Y1 be non empty V144() SubSpace of Y; :: thesis: ( Y0 is SubSpace of Y1 implies Y0 is V144() )

reconsider A1 = the carrier of Y1, A0 = the carrier of Y0 as non empty Subset of Y by Lm3;

assume A1: Y0 is SubSpace of Y1 ; :: thesis: Y0 is V144()

A2: A1 is T_0 by Th13;

( [#] Y0 = A0 & [#] Y1 = A1 ) ;

then A0 c= A1 by A1, PRE_TOPC:def 4;

then A0 is T_0 by A2;

hence Y0 is V144() ; :: thesis: verum