environ
vocabularies HIDDEN, XCMPLX_0, ARYTM_3, CARD_1, NUMBERS, SUBSET_1, ARYTM_0, ARYTM_1, RELAT_1;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0;
definitions ;
theorems ARYTM_0, XCMPLX_0, NUMBERS;
schemes ;
registrations XCMPLX_0, ORDINAL1;
constructors HIDDEN, FUNCT_4, ARYTM_0, XCMPLX_0, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities ;
expansions ;
0 in NAT
;
then reconsider Z = 0 as Element of REAL by NUMBERS:19;
1 in NAT
;
then reconsider J = 1 as Element of REAL by NUMBERS:19;
Lm1:
- 0 = 0
Lm2:
opp Z = 0
Lm3:
1 " = 1