begin
:: deftheorem defines + MATHMORP:def 1 :
:: deftheorem defines ! MATHMORP:def 2 :
:: deftheorem defines (-) MATHMORP:def 3 :
:: deftheorem defines (+) MATHMORP:def 4 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
Lm1:
for n being Element of NAT
for x, y being Point of (TOP-REAL n) holds {x} + y = {y} + x
theorem
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem
Lm2:
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds (X (-) B) (+) B c= X
theorem Th23:
theorem
theorem
theorem
theorem Th27:
theorem Th28:
theorem
theorem
theorem
theorem
theorem
theorem Th34:
theorem
theorem
theorem Th37:
theorem Th38:
begin
:: deftheorem defines (O) MATHMORP:def 5 :
:: deftheorem defines (o) MATHMORP:def 6 :
theorem
theorem
theorem Th41:
theorem Th42:
theorem
theorem
theorem Th45:
theorem Th46:
theorem
theorem
theorem
theorem Th50:
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem defines (.) MATHMORP:def 7 :
theorem
theorem
theorem Th58:
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem
begin
:: deftheorem defines (*) MATHMORP:def 8 :
:: deftheorem defines (&) MATHMORP:def 9 :
:: deftheorem defines (@) MATHMORP:def 10 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
begin
theorem Th75:
:: deftheorem Def11 defines convex MATHMORP:def 11 :
theorem
theorem Th77:
theorem
theorem