environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, ARYTM_3, STRUCT_0, REALSET1, ARYTM_1, VALUED_2, TARSKI, SUPINF_2, XBOOLE_0, RELAT_1, CARD_1, MONOID_0, RLVECT_1, CONVEX1, XXREAL_0, REAL_1, RLTOPSP1, MATHMORP, ALGSTR_0;
notations HIDDEN, TARSKI, ORDINAL1, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, XREAL_0, REAL_1, RLVECT_1, RLTOPSP1, EUCLID, RUSUB_4;
definitions TARSKI, XBOOLE_0;
theorems XBOOLE_1, XCMPLX_1, TARSKI, SUBSET_1, ZFMISC_1, XBOOLE_0, JORDAN1, XREAL_1, RLTOPSP1, RLVECT_1, RLVECT_4;
schemes ;
registrations XXREAL_0, XREAL_0, STRUCT_0, EUCLID, RLVECT_1, ORDINAL1;
constructors HIDDEN, DOMAIN_1, REAL_1, JORDAN1, CONVEX1, BINOP_2, RUSUB_4;
requirements HIDDEN, REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
equalities XBOOLE_0, SUBSET_1, ALGSTR_0, RUSUB_4;
expansions TARSKI, XBOOLE_0;
Lm1:
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x, y being Point of T holds {x} + y = {y} + x
Lm2:
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x, p being Point of T holds
( (p - x) + x = p & (p + x) - x = p )
Lm3:
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (-) B) (+) B c= X
:: Translation of X according to p