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 ( R0 S in D & R2 S in D & R3a S in D & R3b S in D ) by DefRank;
hence D is 0 -ranked by DefRank; :: thesis: verum