:: Some Properties of Binary Relations
:: by Waldemar Korczy\'nski
::
:: Received January 17, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem :: SYSREL:1
canceled;
theorem :: SYSREL:2
canceled;
theorem :: SYSREL:3
canceled;
theorem :: SYSREL:4
canceled;
theorem :: SYSREL:5
canceled;
theorem :: SYSREL:6
canceled;
theorem :: SYSREL:7
canceled;
theorem :: SYSREL:8
canceled;
theorem :: SYSREL:9
canceled;
theorem :: SYSREL:10
canceled;
theorem :: SYSREL:11
canceled;
theorem Th12: :: SYSREL:12
theorem Th13: :: SYSREL:13
theorem :: SYSREL:14
theorem Th15: :: SYSREL:15
theorem :: SYSREL:16
theorem :: SYSREL:17
canceled;
theorem :: SYSREL:18
theorem :: SYSREL:19
canceled;
theorem Th20: :: SYSREL:20
theorem :: SYSREL:21
canceled;
theorem :: SYSREL:22
for
X,
Y,
x,
y being
set for
R being
Relation holds
( (
X misses Y &
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R &
x in X implies ( not
x in Y & not
y in X &
y in Y ) ) & (
X misses Y &
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R &
y in Y implies ( not
y in X & not
x in Y &
x in X ) ) & (
X misses Y &
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R &
x in Y implies ( not
x in X & not
y in Y &
y in X ) ) & (
X misses Y &
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R &
y in X implies ( not
x in X & not
y in Y &
x in Y ) ) )
theorem :: SYSREL:23
canceled;
theorem Th24: :: SYSREL:24
theorem :: SYSREL:25
theorem :: SYSREL:26
theorem :: SYSREL:27
Lm1:
for X being set holds id X c= [:X,X:]
theorem :: SYSREL:28
canceled;
theorem Th29: :: SYSREL:29
theorem :: SYSREL:30
theorem :: SYSREL:31
canceled;
theorem Th32: :: SYSREL:32
theorem Th33: :: SYSREL:33
theorem :: SYSREL:34
theorem :: SYSREL:35
theorem :: SYSREL:36
theorem :: SYSREL:37
theorem :: SYSREL:38
theorem :: SYSREL:39
theorem Th40: :: SYSREL:40
theorem :: SYSREL:41
theorem :: SYSREL:42
:: deftheorem defines CL SYSREL:def 1 :
theorem :: SYSREL:43
canceled;
theorem Th44: :: SYSREL:44
theorem Th45: :: SYSREL:45
theorem Th46: :: SYSREL:46
theorem Th47: :: SYSREL:47
theorem Th48: :: SYSREL:48
theorem :: SYSREL:49
theorem :: SYSREL:50
theorem Th51: :: SYSREL:51
theorem :: SYSREL:52
theorem Th53: :: SYSREL:53
theorem Th54: :: SYSREL:54
theorem :: SYSREL:55
theorem :: SYSREL:56
theorem Th57: :: SYSREL:57
theorem Th58: :: SYSREL:58
theorem :: SYSREL:59