environ
vocabularies HIDDEN, NUMBERS, XREAL_0, XCMPLX_0, FUNCT_3, SQUARE_1, ARYTM_1, RELAT_1, REAL_1, CARD_1, ARYTM_3, XXREAL_0;
notations HIDDEN, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, XXREAL_0;
definitions ;
theorems SQUARE_1, XCMPLX_1, XREAL_1, XXREAL_0;
schemes ;
registrations XCMPLX_0, XREAL_0, SQUARE_1, MEMBERED;
constructors HIDDEN, SQUARE_1, MEMBERED, XXREAL_0;
requirements HIDDEN, REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities SQUARE_1;
expansions ;
Lm1:
for a, b being Complex holds
( not a ^2 = b ^2 or a = b or a = - b )