set R = the strict Refinement of T,S;
take the strict Refinement of T,S ; :: thesis: ( the strict Refinement of T,S is strict & not the strict Refinement of T,S is empty )
thus ( the strict Refinement of T,S is strict & not the strict Refinement of T,S is empty ) ; :: thesis: verum