environ
vocabularies HIDDEN, NUMBERS, FINSET_1, XBOOLE_0, CARD_1, XXREAL_0, SUBSET_1, TARSKI, ORDINAL1, SETFAM_1, ZFMISC_1, EQREL_1, NAT_1, FUNCT_1, FINSEQ_1, ARYTM_3, RELAT_1, ORDERS_2, RELAT_2, COMBGRAS, STRUCT_0, ORDERS_1, CIRCUIT2, GROUP_10, RAMSEY_1, JORDAN4, WAYBEL_0, WAYBEL_4, YELLOW_0, FUNCT_2, LEXBFS, ARYTM_1, UPROOTS, CARD_3, FINSEQ_2, VALUED_0, SQUARE_1, ORDINAL2, DILWORTH, REAL_1;
notations HIDDEN, TARSKI, RELAT_1, RELAT_2, RELSET_1, FINSET_1, SETFAM_1, XBOOLE_0, SUBSET_1, CARD_1, STRUCT_0, WAYBEL_0, WAYBEL_4, ORDERS_2, ORDINAL1, EQREL_1, FUNCT_1, FUNCT_2, NUMBERS, XREAL_0, XXREAL_0, NAT_1, YELLOW_0, XCMPLX_0, ZFMISC_1, LEXBFS, FINSEQ_1, SQUARE_1, UPROOTS, RVSUM_1, INT_5, FINSEQ_2, VALUED_0, GROUP_10, RAMSEY_1, DOMAIN_1;
definitions TARSKI, FUNCT_1, RELAT_2, XBOOLE_0, VALUED_0, ORDERS_2;
theorems CARD_1, CARD_2, NAT_1, XREAL_1, YELLOW_0, XBOOLE_0, TARSKI, ORDERS_2, XBOOLE_1, ZFMISC_1, EQREL_1, INT_1, EULER_1, ENUMSET1, FUNCT_1, FUNCT_2, LEXBFS, FINSEQ_4, BAGORDER, WAYBEL_0, WAYBEL_4, XXREAL_0, RELAT_1, ORDERS_1, FINSET_1, ORDINAL1, PUA2MSS1, DICKSON, FINSEQ_1, INT_5, RVSUM_1, FINSEQ_2, CARD_3, FINSEQ_3, GRFUNC_1, RAMSEY_1, SUBSET_1, PRE_POLY, XTUPLE_0, NUMBERS;
schemes NAT_1, FUNCT_2, XBOOLE_0, CLASSES1, FRAENKEL, TREES_2, RELSET_1;
registrations STRUCT_0, XXREAL_0, RELSET_1, CARD_1, YELLOW_0, XREAL_0, FINSET_1, XBOOLE_0, NAT_1, INT_1, YELLOW_2, EQREL_1, FINSEQ_1, FUNCT_1, SUBSET_1, ORDINAL1, PEPIN, RVSUM_1, FUNCT_2, FINSEQ_2, NUMBERS, RELAT_1, VALUED_0, ORDERS_2;
constructors HIDDEN, DOMAIN_1, LEXBFS, WAYBEL_4, SQUARE_1, UPROOTS, WSIERP_1, INT_5, RAMSEY_1, RELSET_1, BINOP_2, NUMBERS;
requirements HIDDEN, ARITHM, SUBSET, BOOLE, NUMERALS, REAL;
equalities STRUCT_0, WAYBEL_0, SQUARE_1, GROUP_10, CARD_1, ORDINAL1;
expansions TARSKI, STRUCT_0, FUNCT_1, RELAT_2, XBOOLE_0, ORDERS_2;
theorem Th1:
for
X,
Y,
x being
set st not
x in X holds
X \ (Y \/ {x}) = X \ Y