% Mizar problem: t66_classes1,classes1,1530,28 
fof(t66_classes1,conjecture,(
    ! [A] : k5_classes1(k5_classes1(A)) = k5_classes1(A) ),
    inference(mizar_bg_added,[status(thm)],[dt_k5_classes1,t58_classes1,t62_classes1]),
    [file(classes1,t66_classes1)]).

fof(dt_k5_classes1,axiom,(
    $true ),
    file(classes1,k5_classes1),
    []).

fof(t58_classes1,axiom,(
    ! [A] : v1_ordinal1(k5_classes1(A)) ),
    file(classes1,t58_classes1),
    []).

fof(t62_classes1,axiom,(
    ! [A] : 
      ( v1_ordinal1(A)
     => k5_classes1(A) = A ) ),
    file(classes1,t62_classes1),
    []).