environ
vocabularies HIDDEN, ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, SUBSET_1, ORDINAL3, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1, ORDINAL2;
definitions ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, ORDINAL1, SETFAM_1, ORDINAL2, XBOOLE_1, ZFMISC_1;
schemes ORDINAL1, ORDINAL2, XBOOLE_0;
registrations XBOOLE_0, ORDINAL1, ORDINAL2;
constructors HIDDEN, SETFAM_1, ORDINAL2, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities ORDINAL2, ORDINAL1;
expansions ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0;
Lm1:
1 = succ 0
;
theorem
for
A,
B being
Ordinal st
A *^ B = 1 holds
(
A = 1 &
B = 1 )
theorem Th48:
for
A,
C1,
D1,
C2,
D2 being
Ordinal st
(C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 &
D1 in A &
D2 in A holds
(
C1 = C2 &
D1 = D2 )