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