begin
theorem
for
x,
y,
A,
B being
set st
x in A \/ B &
y in A \/ B & not (
x in A \ B &
y in A \ B ) & not (
x in B &
y in B ) & not (
x in A \ B &
y in B ) holds
(
x in B &
y in A \ B )
:: deftheorem Def1 defines tolerates LATSUM_1:def 1 :
begin
:: deftheorem Def2 defines [*] LATSUM_1:def 2 :
theorem Th2:
theorem Th3:
begin
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
theorem Th21:
theorem
theorem
theorem
theorem