:: The Operation of Addition of Relational Structures
:: by Katarzyna Romanowicz and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: LATSUM_1:1
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 :
:: deftheorem Def2 defines [*] LATSUM_1:def 2 :
theorem Th2: :: LATSUM_1:2
theorem Th3: :: LATSUM_1:3
theorem Th4: :: LATSUM_1:4
theorem Th5: :: LATSUM_1:5
theorem Th6: :: LATSUM_1:6
theorem :: LATSUM_1:7
theorem Th8: :: LATSUM_1:8
theorem Th9: :: LATSUM_1:9
theorem Th10: :: LATSUM_1:10
theorem :: LATSUM_1:11
theorem Th12: :: LATSUM_1:12
theorem Th13: :: LATSUM_1:13
theorem :: LATSUM_1:14
theorem Th15: :: LATSUM_1:15
theorem Th16: :: LATSUM_1:16
theorem Th17: :: LATSUM_1:17
theorem Th18: :: LATSUM_1:18
theorem :: LATSUM_1:19
theorem :: LATSUM_1:20
theorem Th21: :: LATSUM_1:21
theorem :: LATSUM_1:22
theorem :: LATSUM_1:23
theorem :: LATSUM_1:24
theorem :: LATSUM_1:25