take the 1 -ranked RuleSet of S ; :: thesis: the 1 -ranked RuleSet of S is 0 -ranked
thus the 1 -ranked RuleSet of S is 0 -ranked ; :: thesis: verum