Example Annotated Formulae

fof(formula_27,axiom,
    ! [X,Y] : 
      ( subclass(X,Y) <=> 
        ! [U] : 
          ( member(U,X) => member(U,Y) )),
    file('SET005+0.ax',subclass_defn),
    [description('Definition of subclass'), relevance(0.9)]).

cnf(175,lemma,
    ( rsymProp(ib,sk_c3)
    | sk_c4 = sk_c3 ),
    inference(factor_simp,[status(thm)],[
        inference(para_into,[status(thm)],[96,78])]),
    [iquote('para_into,96.2.1,78.1.1,factor_simp')]).