% Mizar problem: e2_55_1,lfuzzy_0,1527,12 
include('Axioms/SET010^2.ax').
thf(f1_s4_lfuzzy_0_type,type,( f1_s4_lfuzzy_0: $i )).
thf(f2_s4_lfuzzy_0_type,type,( f2_s4_lfuzzy_0: $i )).
thf(f3_s4_lfuzzy_0_type,type,( f3_s4_lfuzzy_0: $i > $i > $i )).
thf(f4_s4_lfuzzy_0_type,type,( f4_s4_lfuzzy_0: $i > $i > $i )).
thf(m1_subset_1_type,type,( m1_subset_1: $i > $i > $o )).
thf(p1_s4_lfuzzy_0_type,type,( p1_s4_lfuzzy_0: $i > $i > $o )).
thf(v1_int_1_type,type,( v1_int_1: $i > $o )).
thf(v1_membered_type,type,( v1_membered: $i > $o )).
thf(v1_rat_1_type,type,( v1_rat_1: $i > $o )).
thf(v1_xboole_0_type,type,( v1_xboole_0: $i > $o )).
thf(v1_xcmplx_0_type,type,( v1_xcmplx_0: $i > $o )).
thf(v1_xreal_0_type,type,( v1_xreal_0: $i > $o )).
thf(v1_xxreal_0_type,type,( v1_xxreal_0: $i > $o )).
thf(v2_membered_type,type,( v2_membered: $i > $o )).
thf(v3_membered_type,type,( v3_membered: $i > $o )).
thf(v4_membered_type,type,( v4_membered: $i > $o )).
thf(v5_membered_type,type,( v5_membered: $i > $o )).
thf(v6_membered_type,type,( v6_membered: $i > $o )).
thf(v7_membered_type,type,( v7_membered: $i > $o )).
thf(v7_ordinal1_type,type,( v7_ordinal1: $i > $o )).
thf(cc12_membered,axiom,( ! [A: $i] : ( ( v1_membered @ A ) => ! [B: $i] : ( ( m1_subset_1 @ B @ A ) => ( v1_xcmplx_0 @ B ) ) ) ),file(membered,cc12_membered)).
thf(cc13_membered,axiom,( ! [A: $i] : ( ( v2_membered @ A ) => ! [B: $i] : ( ( m1_subset_1 @ B @ A ) => ( v1_xxreal_0 @ B ) ) ) ),file(membered,cc13_membered)).
thf(cc14_membered,axiom,( ! [A: $i] : ( ( v3_membered @ A ) => ! [B: $i] : ( ( m1_subset_1 @ B @ A ) => ( v1_xreal_0 @ B ) ) ) ),file(membered,cc14_membered)).
thf(cc4_membered,axiom,( ! [A: $i] : ( ( v3_membered @ A ) => ( v2_membered @ A ) ) ),file(membered,cc4_membered)).
thf(cc5_membered,axiom,( ! [A: $i] : ( ( v3_membered @ A ) => ( v1_membered @ A ) ) ),file(membered,cc5_membered)).
thf(rc4_xreal_0,axiom,( ? [A: $i] : ( ( v1_xboole_0 @ A ) & ( v1_xcmplx_0 @ A ) & ( v1_xxreal_0 @ A ) & ( v1_xreal_0 @ A ) ) ),file(xreal_0,rc4_xreal_0)).
thf(cc15_membered,axiom,( ! [A: $i] : ( ( v4_membered @ A ) => ! [B: $i] : ( ( m1_subset_1 @ B @ A ) => ( v1_rat_1 @ B ) ) ) ),file(membered,cc15_membered)).
thf(cc3_membered,axiom,( ! [A: $i] : ( ( v4_membered @ A ) => ( v3_membered @ A ) ) ),file(membered,cc3_membered)).
thf(cc3_xreal_0,axiom,( ! [A: $i] : ( ( v1_xreal_0 @ A ) => ( v1_xcmplx_0 @ A ) ) ),file(xreal_0,cc3_xreal_0)).
thf(cc4_xreal_0,axiom,( ! [A: $i] : ( ( v1_xreal_0 @ A ) => ( v1_xxreal_0 @ A ) ) ),file(xreal_0,cc4_xreal_0)).
thf(rc1_xreal_0,axiom,( ? [A: $i] : ( v1_xreal_0 @ A ) ),file(xreal_0,rc1_xreal_0)).
thf(cc16_membered,axiom,( ! [A: $i] : ( ( v5_membered @ A ) => ! [B: $i] : ( ( m1_subset_1 @ B @ A ) => ( v1_int_1 @ B ) ) ) ),file(membered,cc16_membered)).
thf(cc2_membered,axiom,( ! [A: $i] : ( ( v5_membered @ A ) => ( v4_membered @ A ) ) ),file(membered,cc2_membered)).
thf(cc2_xreal_0,axiom,( ! [A: $i] : ( ( v7_ordinal1 @ A ) => ( v1_xreal_0 @ A ) ) ),file(xreal_0,cc2_xreal_0)).
thf(cc17_membered,axiom,( ! [A: $i] : ( ( v6_membered @ A ) => ! [B: $i] : ( ( m1_subset_1 @ B @ A ) => ( v7_ordinal1 @ B ) ) ) ),file(membered,cc17_membered)).
thf(cc1_membered,axiom,( ! [A: $i] : ( ( v6_membered @ A ) => ( v5_membered @ A ) ) ),file(membered,cc1_membered)).
thf(rc1_membered,axiom,( ? [A: $i] : ( ~ ( v1_xboole_0 @ A ) & ( v6_membered @ A ) ) ),file(membered,rc1_membered)).
thf(rc2_membered,axiom,( ? [A: $i] : ( ~ ( v1_xboole_0 @ A ) & ( v6_membered @ A ) ) ),file(membered,rc2_membered)).
thf(rc3_membered,axiom,( ? [A: $i] : ( ~ ( v1_xboole_0 @ A ) & ( v6_membered @ A ) & ( v7_membered @ A ) ) ),file(membered,rc3_membered)).
thf(cc18_membered,axiom,( ! [A: $i] : ( ( v1_xboole_0 @ A ) => ( v6_membered @ A ) ) ),file(membered,cc18_membered)).
thf(cc26_membered,axiom,( ! [A: $i] : ( ( v1_xboole_0 @ A ) => ( v7_membered @ A ) ) ),file(membered,cc26_membered)).
thf(dt_m1_subset_1,axiom,( $true ),file(subset_1,m1_subset_1)).
thf(dt_f1_s4_lfuzzy_0,axiom,( ~ ( v1_xboole_0 @ f1_s4_lfuzzy_0 ) ),file(lfuzzy_0,f1_s4_lfuzzy_0)).
thf(dt_f2_s4_lfuzzy_0,axiom,( ~ ( v1_xboole_0 @ f2_s4_lfuzzy_0 ) ),file(lfuzzy_0,f2_s4_lfuzzy_0)).
thf(dt_f3_s4_lfuzzy_0,axiom,( $true ),file(lfuzzy_0,f3_s4_lfuzzy_0)).
thf(dt_f4_s4_lfuzzy_0,axiom,( $true ),file(lfuzzy_0,f4_s4_lfuzzy_0)).
thf(e2_55__lfuzzy_0,axiom,( ! [A: $i] : ( ( m1_subset_1 @ A @ f1_s4_lfuzzy_0 ) => ! [B: $i] : ( ( m1_subset_1 @ B @ f2_s4_lfuzzy_0 ) => ( ( p1_s4_lfuzzy_0 @ A @ B ) => ( = @ ( f3_s4_lfuzzy_0 @ A @ B ) @ ( f4_s4_lfuzzy_0 @ A @ B ) ) ) ) ) ),file(lfuzzy_0,e2_55__lfuzzy_0)).
thf(s3_lfuzzy_0,axiom,( ! [A: $i > $i > $i] : ! [B: $i > $i > $i] : ! [C: $i > $i > $o] : ! [D: $i] : ! [E: $i] : ( ( ~ ( v1_xboole_0 @ E ) & ~ ( v1_xboole_0 @ D ) ) => ( ! [F: $i] : ( ( m1_subset_1 @ F @ E ) => ! [G: $i] : ( ( m1_subset_1 @ G @ D ) => ( ( C @ F @ G ) => ( = @ ( B @ F @ G ) @ ( A @ F @ G ) ) ) ) ) => ( = @ ( replSep2 @ ^ [F: $i] : ( m1_subset_1 @ F @ E ) @ ^ [F: $i] : ^ [G: $i] : ( m1_subset_1 @ G @ D ) @ ^ [F: $i] : ^ [G: $i] : ( B @ F @ G ) @ ^ [F: $i] : ^ [G: $i] : ( C @ F @ G ) ) @ ( replSep2 @ ^ [F: $i] : ( m1_subset_1 @ F @ E ) @ ^ [F: $i] : ^ [G: $i] : ( m1_subset_1 @ G @ D ) @ ^ [F: $i] : ^ [G: $i] : ( A @ F @ G ) @ ^ [F: $i] : ^ [G: $i] : ( C @ F @ G ) ) ) ) ) ),file(lfuzzy_0,s3_lfuzzy_0)).
thf(e2_55_1__lfuzzy_0,conjecture,( = @ ( replSep2 @ ^ [A: $i] : ( m1_subset_1 @ A @ f1_s4_lfuzzy_0 ) @ ^ [A: $i] : ^ [B: $i] : ( m1_subset_1 @ B @ f2_s4_lfuzzy_0 ) @ ^ [A: $i] : ^ [B: $i] : ( f3_s4_lfuzzy_0 @ A @ B ) @ ^ [A: $i] : ^ [B: $i] : ( p1_s4_lfuzzy_0 @ A @ B ) ) @ ( replSep2 @ ^ [A: $i] : ( m1_subset_1 @ A @ f1_s4_lfuzzy_0 ) @ ^ [A: $i] : ^ [B: $i] : ( m1_subset_1 @ B @ f2_s4_lfuzzy_0 ) @ ^ [A: $i] : ^ [B: $i] : ( f4_s4_lfuzzy_0 @ A @ B ) @ ^ [A: $i] : ^ [B: $i] : ( p1_s4_lfuzzy_0 @ A @ B ) ) ),file(lfuzzy_0,e2_55_1__lfuzzy_0)).
thf(sethood_m1_subset_1,axiom,( ! [A: $i] : ( sethood @ ^ [X: $i] : ( m1_subset_1 @ X @ A ) ) ),file(subset_1,m1_subset_1)).
