:: YELLOW_4 semantic presentation
theorem Th1: :: YELLOW_4:1
theorem Th2: :: YELLOW_4:2
:: deftheorem Def1 defines is_finer_than YELLOW_4:def 1 :
:: deftheorem Def2 defines is_coarser_than YELLOW_4:def 2 :
theorem Th3: :: YELLOW_4:3
theorem Th4: :: YELLOW_4:4
theorem Th5: :: YELLOW_4:5
theorem Th6: :: YELLOW_4:6
theorem Th7: :: YELLOW_4:7
theorem Th8: :: YELLOW_4:8
:: deftheorem Def3 defines "\/" YELLOW_4:def 3 :
theorem Th9: :: YELLOW_4:9
theorem Th10: :: YELLOW_4:10
theorem Th11: :: YELLOW_4:11
theorem Th12: :: YELLOW_4:12
theorem Th13: :: YELLOW_4:13
theorem Th14: :: YELLOW_4:14
theorem Th15: :: YELLOW_4:15
theorem Th16: :: YELLOW_4:16
theorem Th17: :: YELLOW_4:17
theorem Th18: :: YELLOW_4:18
theorem Th19: :: YELLOW_4:19
theorem Th20: :: YELLOW_4:20
theorem Th21: :: YELLOW_4:21
theorem Th22: :: YELLOW_4:22
theorem Th23: :: YELLOW_4:23
theorem Th24: :: YELLOW_4:24
theorem Th25: :: YELLOW_4:25
theorem Th26: :: YELLOW_4:26
theorem Th27: :: YELLOW_4:27
theorem Th28: :: YELLOW_4:28
theorem Th29: :: YELLOW_4:29
theorem Th30: :: YELLOW_4:30
theorem Th31: :: YELLOW_4:31
theorem Th32: :: YELLOW_4:32
theorem Th33: :: YELLOW_4:33
theorem Th34: :: YELLOW_4:34
theorem Th35: :: YELLOW_4:35
:: deftheorem Def4 defines "/\" YELLOW_4:def 4 :
theorem Th36: :: YELLOW_4:36
theorem Th37: :: YELLOW_4:37
theorem Th38: :: YELLOW_4:38
theorem Th39: :: YELLOW_4:39
theorem Th40: :: YELLOW_4:40
theorem Th41: :: YELLOW_4:41
theorem Th42: :: YELLOW_4:42
theorem Th43: :: YELLOW_4:43
theorem Th44: :: YELLOW_4:44
theorem Th45: :: YELLOW_4:45
theorem Th46: :: YELLOW_4:46
theorem Th47: :: YELLOW_4:47
theorem Th48: :: YELLOW_4:48
theorem Th49: :: YELLOW_4:49
theorem Th50: :: YELLOW_4:50
theorem Th51: :: YELLOW_4:51
theorem Th52: :: YELLOW_4:52
theorem Th53: :: YELLOW_4:53
theorem Th54: :: YELLOW_4:54
theorem Th55: :: YELLOW_4:55
theorem Th56: :: YELLOW_4:56
theorem Th57: :: YELLOW_4:57
theorem Th58: :: YELLOW_4:58
theorem Th59: :: YELLOW_4:59
theorem Th60: :: YELLOW_4:60
theorem Th61: :: YELLOW_4:61
theorem Th62: :: YELLOW_4:62
theorem Th63: :: YELLOW_4:63
theorem Th64: :: YELLOW_4:64