environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, MEMBERED, XCMPLX_0, XXREAL_0, ARYTM_1, RELAT_1, TARSKI, XBOOLE_0, ARYTM_3, RAT_1, INT_1, CARD_1, MEMBER_1, NAT_1, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, RAT_1, INT_1, MEMBERED, XXREAL_3, XXREAL_0;
definitions TARSKI, XBOOLE_0, MEMBERED;
theorems XCMPLX_0, TARSKI, XBOOLE_0, ENUMSET1, XCMPLX_1, XXREAL_0, XXREAL_3;
schemes ;
registrations XREAL_0, INT_1, RAT_1, ORDINAL1, MEMBERED, XCMPLX_0, NAT_1, XXREAL_3, XBOOLE_0;
constructors HIDDEN, XCMPLX_0, RAT_1, MEMBERED, ENUMSET1, BINOP_2, XXREAL_3;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities XBOOLE_0, XCMPLX_0, XXREAL_3;
expansions MEMBERED;
Lm1:
for F, G being ext-real-membered set st F c= G holds
-- F c= -- G
Lm2:
for A, B being complex-membered set st A c= B holds
-- A c= -- B
Lm3:
for A, B being complex-membered set st A c= B holds
A "" c= B ""
Lm4:
for F, G being ext-real-membered set holds -- (F ++ G) = (-- F) ++ (-- G)
Lm5:
for A, B being complex-membered set holds -- (A ++ B) = (-- A) ++ (-- B)