begin
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
theorem Th1:
:: deftheorem Def1 defines circled CIRCLED1:def 1 :
theorem Th2:
theorem Th3:
theorem
theorem
theorem Th6:
theorem
theorem
begin
:: deftheorem Def2 defines Circled-Family CIRCLED1:def 2 :
:: deftheorem defines Cir CIRCLED1:def 3 :
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem
theorem Th14:
theorem
begin
:: deftheorem Def4 defines circled CIRCLED1:def 4 :
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
:: deftheorem defines circledComb CIRCLED1:def 5 :
:: deftheorem defines circledComb CIRCLED1:def 6 :
theorem
theorem
theorem
theorem Th24:
theorem Th25:
theorem
theorem