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