% Mizar problem: e1_55_2_1,dilworth,1268,56 
include('Axioms/SET010^0.ax').
thf(c1_55_type,type,( c1_55__dilworth: $i )).
thf(u1_struct_0_type,type,( u1_struct_0: $i > $i )).
thf(l1_orders_2_type,type,( l1_orders_2: $i > $o )).
thf(l1_struct_0_type,type,( l1_struct_0: $i > $o )).
thf(m1_subset_1_type,type,( m1_subset_1: $i > $i > $o )).
thf(r3_waybel_4_type,type,( r3_waybel_4: $i > $i > $i > $o )).
thf(dt_l1_struct_0,axiom,( $true ),file(struct_0,l1_struct_0)).
thf(antisymmetry_r2_hidden,axiom,( ! [A: $i] : ! [B: $i] : ( ( r2_hidden @ A @ B ) => ~ ( r2_hidden @ B @ A ) ) ),file(hidden,r2_hidden)).
thf(dt_l1_orders_2,axiom,( ! [A: $i] : ( ( l1_orders_2 @ A ) => ( l1_struct_0 @ A ) ) ),file(orders_2,l1_orders_2)).
thf(dt_m1_subset_1,axiom,( $true ),file(subset_1,m1_subset_1)).
thf(dt_u1_struct_0,axiom,( $true ),file(struct_0,u1_struct_0)).
thf(dt_c1_55__dilworth,axiom,( l1_orders_2 @ c1_55__dilworth ),file(dilworth,c1_55__dilworth)).
thf(s1_xboole_0,axiom,( ! [A: $i > $o] : ! [B: $i] : ? [C: $i] : ! [D: $i] : ( ( r2_hidden @ D @ C ) <=> ( ( r2_hidden @ D @ B ) & ( A @ D ) ) ) ),file(xboole_0,s1_xboole_0)).
thf(e1_55_2_1__dilworth,conjecture,( ? [A: $i] : ! [B: $i] : ( ( r2_hidden @ B @ A ) <=> ( ( r2_hidden @ B @ ( u1_struct_0 @ c1_55__dilworth ) ) & ? [C: $i] : ( ( m1_subset_1 @ C @ ( u1_struct_0 @ c1_55__dilworth ) ) & ( = @ C @ B ) & ( r3_waybel_4 @ c1_55__dilworth @ ( u1_struct_0 @ c1_55__dilworth ) @ C ) ) ) ) ),file(dilworth,e1_55_2_1__dilworth)).
