set D = the 1 -ranked RuleSet of S;
reconsider DD = the 1 -ranked RuleSet of S as 0 -ranked RuleSet of S ;
take DD ; :: thesis: DD is 1 -ranked
thus DD is 1 -ranked ; :: thesis: verum