let D be RuleSet of S; :: thesis: ( D is 2 -ranked implies D is 1 -ranked )
assume D is 2 -ranked ; :: thesis: D is 1 -ranked
then ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D ) by Def62;
hence D is 1 -ranked by Def62; :: thesis: verum