environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, RLVECT_1, SUBSET_1, ARYTM_1, RLTOPSP1, REAL_1, COMPLEX1, XXREAL_0, RELAT_1, TARSKI, ARYTM_3, RUSUB_4, RLSUB_1, STRUCT_0, SUPINF_2, SETFAM_1, CARD_1, PRE_TOPC, RLVECT_2, FINSEQ_1, FUNCT_1, CARD_3, NAT_1, FUNCT_2, VALUED_1, ORDINAL4, PARTFUN1, CIRCLED1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, FUNCT_1, SETFAM_1, PARTFUN1, FUNCT_2, XXREAL_0, REAL_1, DOMAIN_1, STRUCT_0, PRE_TOPC, RLVECT_1, RUSUB_4, CONVEX1, FINSEQ_1, RLSUB_1, RLVECT_2, RVSUM_1, RLTOPSP1, RUSUB_5;
definitions TARSKI, XBOOLE_0, RLTOPSP1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, SETFAM_1, XCMPLX_0, FUNCT_1, RLVECT_1, RUSUB_4, CONVEX1, RLTOPSP1, RVSUM_1, FINSEQ_1, RLSUB_1, RUSUB_5, RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4, CARD_2, XREAL_1, FINSOP_1, PARTFUN1, RLVECT_4, XREAL_0;
schemes XBOOLE_0, FINSEQ_1, SUBSET_1;
registrations SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, STRUCT_0, RLVECT_1, RLTOPSP1, VALUED_0, FINSEQ_1, CARD_1, ORDINAL1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, REAL_1, BINOP_2, COMPLEX1, FINSOP_1, RVSUM_1, RUSUB_5, CONVEX1, RLTOPSP1, RELSET_1, NUMBERS;
requirements HIDDEN, BOOLE, REAL, NUMERALS, SUBSET, ARITHM;
equalities XBOOLE_0, RVSUM_1;
expansions TARSKI, XBOOLE_0, RLTOPSP1;
Lm1:
for V being non empty RLSStruct
for M, N being Subset of V
for x, y being VECTOR of V st x in M & y in N holds
x - y in M - N
reconsider jj = 1, jd = 1 / 2 as Element of REAL by XREAL_0:def 1;