environ
vocabularies HIDDEN, GROUP_1, XBOOLE_0, SUBSET_1, GROUP_2, PRE_TOPC, RELAT_1, TARSKI, STRUCT_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4;
definitions XBOOLE_0, TARSKI;
theorems GROUP_1, GROUP_8, GROUP_2, GROUP_3, XBOOLE_0, XBOOLE_1, GROUP_4, STRUCT_0;
schemes ;
registrations XBOOLE_0, STRUCT_0, GROUP_1, GROUP_2, GROUP_3;
constructors HIDDEN, REALSET2, GROUP_4;
requirements HIDDEN, SUBSET, BOOLE;
equalities GROUP_2, GROUP_4;
expansions TARSKI;