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