consider X0 being non empty trivial strict SubSpace of Y;
take X0 ; :: thesis: ( X0 is strict & X0 is T_0 & not X0 is empty )
thus ( X0 is strict & X0 is T_0 & not X0 is empty ) ; :: thesis: verum