:: Miscellaneous Facts about Relation Structure
:: by Agnieszka Julia Marasik
::
:: Received November 8, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: YELLOW_5:1
theorem Th2: :: YELLOW_5:2
theorem :: YELLOW_5:3
theorem :: YELLOW_5:4
theorem :: YELLOW_5:5
theorem Th6: :: YELLOW_5:6
theorem Th7: :: YELLOW_5:7
theorem Th8: :: YELLOW_5:8
theorem Th9: :: YELLOW_5:9
theorem Th10: :: YELLOW_5:10
theorem Th11: :: YELLOW_5:11
:: deftheorem defines \ YELLOW_5:def 1 :
:: deftheorem defines \+\ YELLOW_5:def 2 :
Lm1:
for L being antisymmetric with_suprema with_infima RelStr
for a, b being Element of L holds a \+\ b = b \+\ a
:: deftheorem Def3 defines meets YELLOW_5:def 3 :
theorem :: YELLOW_5:12
theorem :: YELLOW_5:13
theorem :: YELLOW_5:14
canceled;
theorem :: YELLOW_5:15
canceled;
theorem :: YELLOW_5:16
theorem :: YELLOW_5:17
theorem :: YELLOW_5:18
canceled;
theorem :: YELLOW_5:19
theorem Th20: :: YELLOW_5:20
theorem :: YELLOW_5:21
theorem Th22: :: YELLOW_5:22
theorem :: YELLOW_5:23
theorem :: YELLOW_5:24
theorem :: YELLOW_5:25
theorem :: YELLOW_5:26
theorem :: YELLOW_5:27
theorem Th28: :: YELLOW_5:28
theorem :: YELLOW_5:29
theorem :: YELLOW_5:30
theorem :: YELLOW_5:31
theorem :: YELLOW_5:32
theorem :: YELLOW_5:33
theorem :: YELLOW_5:34
theorem :: YELLOW_5:35
theorem :: YELLOW_5:36
theorem Th37: :: YELLOW_5:37
theorem :: YELLOW_5:38
theorem Th39: :: YELLOW_5:39
theorem Th40: :: YELLOW_5:40
theorem :: YELLOW_5:41
theorem :: YELLOW_5:42
theorem :: YELLOW_5:43
theorem :: YELLOW_5:44
theorem :: YELLOW_5:45
theorem :: YELLOW_5:46
theorem :: YELLOW_5:47
theorem :: YELLOW_5:48
theorem :: YELLOW_5:49
theorem :: YELLOW_5:50
theorem :: YELLOW_5:51
theorem :: YELLOW_5:52
theorem :: YELLOW_5:53
theorem :: YELLOW_5:54
theorem :: YELLOW_5:55
theorem :: YELLOW_5:56
theorem :: YELLOW_5:57
theorem :: YELLOW_5:58
theorem :: YELLOW_5:59
theorem :: YELLOW_5:60
theorem :: YELLOW_5:61
theorem :: YELLOW_5:62
theorem :: YELLOW_5:63
theorem :: YELLOW_5:64
theorem Th65: :: YELLOW_5:65
theorem :: YELLOW_5:66
theorem :: YELLOW_5:67
theorem :: YELLOW_5:68
theorem :: YELLOW_5:69
theorem :: YELLOW_5:70
theorem :: YELLOW_5:71
theorem :: YELLOW_5:72