environ
vocabularies HIDDEN, NUMBERS, NAT_1, CARD_1, ZFMISC_1, XBOOLE_0, SUBSET_1, ARYTM_3, FUNCT_3, FUNCT_1, RELAT_1, FUNCT_2, FUNCT_4, TARSKI, FUNCOP_1, ORDERS_2, STRUCT_0, RELAT_2, XXREAL_0, ARYTM_1, WELLORD1, CAT_1, SEQM_3, FINSET_1, ORDINAL1, CARD_2, SQUARE_1, NECKLACE, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, CARD_2, WELLORD1, FINSET_1, SQUARE_1, QUIN_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, REAL_1, NAT_1, NAT_D, RELAT_1, RELAT_2, FUNCT_3, FUNCOP_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, BINOP_1, XXREAL_0, STRUCT_0, ORDERS_2, WAYBEL_0, WAYBEL_1, ORDERS_3;
definitions WAYBEL_0, WAYBEL_1, ORDERS_3, STRUCT_0, FUNCT_1, RELAT_1, RELAT_2, XBOOLE_0, TARSKI;
theorems FUNCT_1, FUNCT_2, FUNCT_4, ENUMSET1, RELSET_1, ZFMISC_1, NAT_1, AXIOMS, CARD_1, WAYBEL_0, SUBSET_1, XBOOLE_0, XBOOLE_1, QUIN_1, WELLORD2, RELAT_1, FUNCT_3, TARSKI, FUNCOP_1, ORDERS_2, RELAT_2, ORDINAL1, CARD_2, SQUARE_1, PARTFUN1, XREAL_1, XXREAL_0, FRECHET, XTUPLE_0;
schemes NAT_1, FRAENKEL, FUNCT_7;
registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1, FUNCT_4, FINSET_1, XREAL_0, SQUARE_1, STRUCT_0, ORDERS_2, HILBERT3, CARD_1, RELAT_1, QUIN_1, NAT_1;
constructors HIDDEN, WELLORD1, REAL_1, SQUARE_1, NAT_1, QUIN_1, CARD_2, REALSET1, ORDERS_3, WAYBEL_1, NAT_D, RELSET_1, FUNCT_4;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
equalities STRUCT_0, XBOOLE_0, SQUARE_1, FUNCOP_1, WELLORD1, SUBSET_1, BINOP_1, CARD_1, ORDINAL1;
expansions WAYBEL_1, RELAT_2;
theorem
for
x1,
x2,
x3,
y1,
y2,
y3 being
set holds
[:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
theorem Th9:
for
a,
b,
c,
d being
set holds
not ( (
a = b implies
c = d ) & (
c = d implies
a = b ) & not
((a,b) --> (c,d)) " = (
c,
d)
--> (
a,
b) )
Lm1:
for S, R being non empty RelStr st S,R are_isomorphic holds
card the InternalRel of S = card the InternalRel of R