% Mizar problem: e1_62_1,subset_1,899,13 
include('Axioms/SET010^0.ax').
thf(c1_62_type,type,( c1_62__subset_1: $i )).
thf(m1_subset_1_type,type,( m1_subset_1: $i > $i > $o )).
thf(existence_m1_subset_1,axiom,( ! [A: $i] : ? [B: $i] : ( m1_subset_1 @ B @ A ) ),file(subset_1,m1_subset_1)).
thf(dt_m1_subset_1,axiom,( $true ),file(subset_1,m1_subset_1)).
thf(dt_c1_62__subset_1,axiom,( $true ),file(subset_1,c1_62__subset_1)).
thf(e1_62_1__subset_1,conjecture,( m1_subset_1 @ ( eps @ ^ [A: $i] : ( m1_subset_1 @ A @ c1_62__subset_1 ) ) @ c1_62__subset_1 ),file(subset_1,e1_62_1__subset_1)).
