include('Axioms/SET010^0.ax').
thf(r2_xboole_0_type, type, r2_xboole_0: $i > $i > $o).
thf(k4_numbers_type, type, k4_numbers: $i).
thf(k1_numbers_type, type, k1_numbers: $i).
thf(k3_numbers_type, type, k3_numbers: $i).
thf(r1_tarski_type, type, r1_tarski: $i > $i > $o).
thf(t2_numbers, axiom,   ( (r2_xboole_0 @ k3_numbers)  @ k1_numbers) , file(numbers, t2_numbers)).
thf(l58_xboole_1, axiom,   (! [A: $i] :  (! [B: $i] :  (! [C: $i] :  ( ( ( (r1_tarski @ A)  @ B)  &  ( (r2_xboole_0 @ B)  @ C) )  =>  ( (r2_xboole_0 @ A)  @ C) ) ) ) ) , file(xboole_1, l58_xboole_1)).
thf(l26_numbers, axiom,   ( (r1_tarski @ k4_numbers)  @ k3_numbers) , file(numbers, l26_numbers)).
thf(t5_numbers, conjecture,   ( (r2_xboole_0 @ k4_numbers)  @ k1_numbers) , file(numbers, t5_numbers)).