public static Justification createSubsetJustification(Proposition mainProposition, Proposition matchingProposition) {
    { Surrogate mainOperator = ((Surrogate)(mainProposition.operator));
      Surrogate matchingOperator = ((Surrogate)(matchingProposition.operator));

      if (!((mainOperator == null) ||
          ((matchingOperator == null) ||
           (mainOperator == matchingOperator)))) {
        if (Logic.relationrefSpecializesRelationrefP(matchingOperator, mainOperator)) {
          { Proposition subsetProposition = null;
            Cons subsetJustifications = Stella.NIL;

            { Object old$Evaluationmode$000 = Logic.$EVALUATIONMODE$.get();

              try {
                Native.setSpecial(Logic.$EVALUATIONMODE$, Logic.KWD_DESCRIPTION);
                subsetProposition = ((Proposition)(Logic.conceiveFormula(Cons.consList(Cons.cons(Logic.SYM_PL_KERNEL_KB_SUBSET_OF, Cons.cons(matchingOperator, Cons.cons(mainOperator, Stella.NIL)))))));

              } finally {
                Logic.$EVALUATIONMODE$.set(old$Evaluationmode$000);
              }
            }
            { PrimitiveStrategy self000 = PrimitiveStrategy.newPrimitiveStrategy();

              self000.proposition = subsetProposition;
              self000.truthValue = Logic.TRUE_TRUTH_VALUE;
              self000.strategy = Logic.KWD_SPECIALIST;
              subsetJustifications = Cons.cons(self000, subsetJustifications);
            }
            { PrimitiveStrategy self001 = PrimitiveStrategy.newPrimitiveStrategy();

              self001.proposition = matchingProposition;
              self001.strategy = Logic.KWD_LOOKUP_ASSERTIONS;
              subsetJustifications = Cons.cons(self001, subsetJustifications);
            }
            { Justification self002 = Justification.newJustification();

              self002.inferenceRule = Logic.KWD_SUBSUMPTION_REASONING;
              self002.proposition = mainProposition;
              self002.antecedents = subsetJustifications;
              { Justification value000 = self002;

                return (value000);
              }
            }
          }
        }
      }
      return (null);
    }
  }