% Mizar problem: t4_pencil_3,pencil_3,125,48 
fof(t4_pencil_3,conjecture,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v3_pencil_1(A)
        & v6_pencil_1(A)
        & l1_pre_topc(A) )
     => ( v10_pencil_1(A)
       => v9_pencil_1(A) ) ) ),
    inference(mizar_bg_added,[status(thm)],[dt_l1_pre_topc,dt_l1_struct_0,existence_l1_pre_topc,existence_l1_struct_0,rc3_struct_0,t28_pencil_1,t3_pencil_3]),
    [file(pencil_3,t4_pencil_3)]).

fof(dt_l1_pre_topc,axiom,(
    ! [A] : 
      ( l1_pre_topc(A)
     => l1_struct_0(A) ) ),
    file(pre_topc,l1_pre_topc),
    []).

fof(dt_l1_struct_0,axiom,(
    $true ),
    file(struct_0,l1_struct_0),
    []).

fof(existence_l1_pre_topc,axiom,(
    ? [A] : l1_pre_topc(A) ),
    file(pre_topc,l1_pre_topc),
    []).

fof(existence_l1_struct_0,axiom,(
    ? [A] : l1_struct_0(A) ),
    file(struct_0,l1_struct_0),
    []).

fof(rc3_struct_0,axiom,(
    ? [A] : 
      ( l1_struct_0(A)
      & ~ v3_struct_0(A) ) ),
    file(struct_0,rc3_struct_0),
    []).

fof(t28_pencil_1,axiom,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v3_pencil_1(A)
        & v6_pencil_1(A)
        & v8_pencil_1(A)
        & l1_pre_topc(A) )
     => ( v10_pencil_1(A)
       => v9_pencil_1(A) ) ) ),
    file(pencil_1,t28_pencil_1),
    []).

fof(t3_pencil_3,axiom,(
    ! [A] : 
      ( ( ~ v3_pencil_1(A)
        & v6_pencil_1(A)
        & l1_pre_topc(A) )
     => ( v10_pencil_1(A)
       => v8_pencil_1(A) ) ) ),
    file(pencil_3,t3_pencil_3),
    []).