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