:: FUZZY_2 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: FUZZY_2:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines \ FUZZY_2:def 1 :
theorem :: FUZZY_2:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th4: :: FUZZY_2:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th25: :: FUZZY_2:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th26: :: FUZZY_2:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def2 defines * FUZZY_2:def 2 :
:: deftheorem Def3 defines ++ FUZZY_2:def 3 :
theorem Th33: :: FUZZY_2:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th34: :: FUZZY_2:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th41: :: FUZZY_2:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm1:
for a, b, c being Real st 0 <= c holds
c * (min a,b) = min (c * a),(c * b)
Lm2:
for a, b, c being Real st 0 <= c holds
c * (max a,b) = max (c * a),(c * b)
theorem :: FUZZY_2:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:48
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:49
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:50
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:51
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:52
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:53
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th54: :: FUZZY_2:54
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:55
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: FUZZY_2:56
:: Showing IDV graph ... (Click the Palm Tree again to close it) 