set X0 = the non empty trivial strict SubSpace of Y;

take the non empty trivial strict SubSpace of Y ; :: thesis: ( the non empty trivial strict SubSpace of Y is strict & the non empty trivial strict SubSpace of Y is T_0 & not the non empty trivial strict SubSpace of Y is empty )

thus ( the non empty trivial strict SubSpace of Y is strict & the non empty trivial strict SubSpace of Y is T_0 & not the non empty trivial strict SubSpace of Y is empty ) ; :: thesis: verum

take the non empty trivial strict SubSpace of Y ; :: thesis: ( the non empty trivial strict SubSpace of Y is strict & the non empty trivial strict SubSpace of Y is T_0 & not the non empty trivial strict SubSpace of Y is empty )

thus ( the non empty trivial strict SubSpace of Y is strict & the non empty trivial strict SubSpace of Y is T_0 & not the non empty trivial strict SubSpace of Y is empty ) ; :: thesis: verum