consider R being strict Refinement of S,T;
take R ; :: thesis: ( R is strict & not R is empty )
thus ( R is strict & not R is empty ) ; :: thesis: verum