:: YELLOW_7 semantic presentation
theorem Th1: :: YELLOW_7:1
theorem Th2: :: YELLOW_7:2
theorem Th3: :: YELLOW_7:3
theorem Th4: :: YELLOW_7:4
theorem Th5: :: YELLOW_7:5
theorem Th6: :: YELLOW_7:6
theorem Th7: :: YELLOW_7:7
theorem Th8: :: YELLOW_7:8
theorem Th9: :: YELLOW_7:9
theorem Th10: :: YELLOW_7:10
theorem Th11: :: YELLOW_7:11
theorem Th12: :: YELLOW_7:12
theorem Th13: :: YELLOW_7:13
theorem Th14: :: YELLOW_7:14
theorem Th15: :: YELLOW_7:15
theorem Th16: :: YELLOW_7:16
theorem Th17: :: YELLOW_7:17
theorem Th18: :: YELLOW_7:18
theorem Th19: :: YELLOW_7:19
theorem Th20: :: YELLOW_7:20
theorem Th21: :: YELLOW_7:21
theorem Th22: :: YELLOW_7:22
theorem Th23: :: YELLOW_7:23
theorem Th24: :: YELLOW_7:24
theorem Th25: :: YELLOW_7:25
theorem Th26: :: YELLOW_7:26
theorem Th27: :: YELLOW_7:27
theorem Th28: :: YELLOW_7:28
theorem Th29: :: YELLOW_7:29
theorem Th30: :: YELLOW_7:30
theorem Th31: :: YELLOW_7:31
theorem Th32: :: YELLOW_7:32
theorem Th33: :: YELLOW_7:33
theorem Th34: :: YELLOW_7:34
theorem Th35: :: YELLOW_7:35
theorem Th36: :: YELLOW_7:36
theorem Th37: :: YELLOW_7:37
:: deftheorem Def1 defines ComplMap YELLOW_7:def 1 :
theorem Th38: :: YELLOW_7:38
theorem Th39: :: YELLOW_7:39
for
b1,
b2 being non
empty RelStr for
b3 being
set holds
( (
b3 is
Function of
b1,
b2 implies
b3 is
Function of
(b1 opp ),
b2 ) & (
b3 is
Function of
(b1 opp ),
b2 implies
b3 is
Function of
b1,
b2 ) & (
b3 is
Function of
b1,
b2 implies
b3 is
Function of
b1,
(b2 opp ) ) & (
b3 is
Function of
b1,
(b2 opp ) implies
b3 is
Function of
b1,
b2 ) & (
b3 is
Function of
b1,
b2 implies
b3 is
Function of
(b1 opp ),
(b2 opp ) ) & (
b3 is
Function of
(b1 opp ),
(b2 opp ) implies
b3 is
Function of
b1,
b2 ) ) ;
theorem Th40: :: YELLOW_7:40
theorem Th41: :: YELLOW_7:41
theorem Th42: :: YELLOW_7:42
theorem Th43: :: YELLOW_7:43
for
b1,
b2 being non
empty RelStr for
b3 being
set holds
( (
b3 is
Connection of
b1,
b2 implies
b3 is
Connection of
b1 ~ ,
b2 ) & (
b3 is
Connection of
b1 ~ ,
b2 implies
b3 is
Connection of
b1,
b2 ) & (
b3 is
Connection of
b1,
b2 implies
b3 is
Connection of
b1,
b2 ~ ) & (
b3 is
Connection of
b1,
b2 ~ implies
b3 is
Connection of
b1,
b2 ) & (
b3 is
Connection of
b1,
b2 implies
b3 is
Connection of
b1 ~ ,
b2 ~ ) & (
b3 is
Connection of
b1 ~ ,
b2 ~ implies
b3 is
Connection of
b1,
b2 ) )
theorem Th44: :: YELLOW_7:44
theorem Th45: :: YELLOW_7:45
theorem Th46: :: YELLOW_7:46
theorem Th47: :: YELLOW_7:47
theorem Th48: :: YELLOW_7:48
theorem Th49: :: YELLOW_7:49
theorem Th50: :: YELLOW_7:50
theorem Th51: :: YELLOW_7:51