:: Propositional Calculus for Boolean Valued Functions, II
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem :: BVFUNC_6:1
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' (b 'imp' (a '&' b)) = I_el Y
proof end;

theorem :: BVFUNC_6:2
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b)) = I_el Y
proof end;

theorem :: BVFUNC_6:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) 'eqv' (b 'or' a) = I_el Y
proof end;

theorem :: BVFUNC_6:4
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c)) = I_el Y
proof end;

theorem :: BVFUNC_6:5
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((a '&' b) 'imp' c) = I_el Y
proof end;

theorem :: BVFUNC_6:6
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b))) = I_el Y
proof end;

theorem :: BVFUNC_6:7
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c)) = I_el Y
proof end;

theorem :: BVFUNC_6:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) 'imp' c)) = I_el Y
proof end;

theorem Th9: :: BVFUNC_6:9
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c) = I_el Y
proof end;

theorem :: BVFUNC_6:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' (b '&' ())) 'imp' () = I_el Y
proof end;

theorem :: BVFUNC_6:11
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' (a 'or' c)) 'imp' (a 'or' (b '&' c)) = I_el Y
proof end;

theorem :: BVFUNC_6:12
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c)) = I_el Y
proof end;

theorem :: BVFUNC_6:13
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c) = I_el Y
proof end;

theorem :: BVFUNC_6:14
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c)) = I_el Y
proof end;

theorem :: BVFUNC_6:15
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a '&' b = I_el Y holds
a 'or' b = I_el Y
proof end;

theorem :: BVFUNC_6:16
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
(a 'or' c) 'imp' (b 'or' c) = I_el Y
proof end;

theorem :: BVFUNC_6:17
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
(a '&' c) 'imp' (b '&' c) = I_el Y
proof end;

theorem th18: :: BVFUNC_6:18
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds
c 'imp' (a '&' b) = I_el Y
proof end;

theorem :: BVFUNC_6:19
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds
(a 'or' b) 'imp' c = I_el Y
proof end;

theorem :: BVFUNC_6:20
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'or' b = I_el Y & 'not' a = I_el Y holds
b = I_el Y
proof end;

theorem tt: :: BVFUNC_6:21
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a '&' c) 'imp' (b '&' d) = I_el Y
proof end;

theorem Th22: :: BVFUNC_6:22
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a 'or' c) 'imp' (b 'or' d) = I_el Y
proof end;

theorem :: BVFUNC_6:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN st (a '&' ()) 'imp' () = I_el Y holds
a 'imp' b = I_el Y
proof end;

theorem :: BVFUNC_6:24
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'imp' () = I_el Y holds
b 'imp' () = I_el Y
proof end;

theorem :: BVFUNC_6:25
for Y being non empty set
for a, b being Function of Y,BOOLEAN st () 'imp' b = I_el Y holds
() 'imp' a = I_el Y
proof end;

theorem Th26: :: BVFUNC_6:26
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'or' b) = I_el Y
proof end;

theorem :: BVFUNC_6:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) 'imp' (() 'imp' b) = I_el Y
proof end;

theorem Th28: :: BVFUNC_6:28
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a 'or' b)) 'imp' (() '&' ()) = I_el Y
proof end;

theorem :: BVFUNC_6:29
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (() '&' ()) 'imp' ('not' (a 'or' b)) = I_el Y
proof end;

theorem :: BVFUNC_6:30
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a 'or' b)) 'imp' () = I_el Y
proof end;

theorem :: BVFUNC_6:31
for Y being non empty set
for a being Function of Y,BOOLEAN holds (a 'or' a) 'imp' a = I_el Y
proof end;

theorem :: BVFUNC_6:32
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' ()) 'imp' b = I_el Y
proof end;

theorem :: BVFUNC_6:33
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (() 'or' b) = I_el Y
proof end;

theorem :: BVFUNC_6:34
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' ('not' (a 'imp' ())) = I_el Y
proof end;

theorem :: BVFUNC_6:35
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a 'imp' ())) 'imp' (a '&' b) = I_el Y
proof end;

theorem Th36: :: BVFUNC_6:36
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a '&' b)) 'imp' (() 'or' ()) = I_el Y
proof end;

theorem :: BVFUNC_6:37
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (() 'or' ()) 'imp' ('not' (a '&' b)) = I_el Y
proof end;

theorem Th38: :: BVFUNC_6:38
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' a = I_el Y
proof end;

theorem :: BVFUNC_6:39
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' (a 'or' b) = I_el Y
proof end;

theorem :: BVFUNC_6:40
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' b = I_el Y
proof end;

theorem :: BVFUNC_6:41
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (a '&' a) = I_el Y
proof end;

theorem Th42: :: BVFUNC_6:42
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'eqv' b) 'imp' (a 'imp' b) = I_el Y
proof end;

theorem :: BVFUNC_6:43
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'eqv' b) 'imp' (b 'imp' a) = I_el Y by Th42;

theorem :: BVFUNC_6:44
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c)) = I_el Y
proof end;

theorem :: BVFUNC_6:45
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' (a '&' (b '&' c)) = I_el Y
proof end;

theorem :: BVFUNC_6:46
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c) = I_el Y
proof end;

theorem :: BVFUNC_6:47
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (() 'imp' b) = b
proof end;

theorem :: BVFUNC_6:48
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' ()) = 'not' a
proof end;

theorem Th73: :: BVFUNC_6:49
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'or' c) = (a 'imp' b) 'or' (a 'imp' c)
proof end;

theorem :: BVFUNC_6:50
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b '&' c) = (a 'imp' b) '&' (a 'imp' c)
proof end;

theorem Th75: :: BVFUNC_6:51
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'imp' c = (a 'imp' c) '&' (b 'imp' c)
proof end;

theorem Th76: :: BVFUNC_6:52
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = (a 'imp' c) 'or' (b 'imp' c)
proof end;

theorem Th7: :: BVFUNC_6:53
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = a 'imp' (b 'imp' c)
proof end;

theorem :: BVFUNC_6:54
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = a 'imp' (() 'or' c)
proof end;

theorem :: BVFUNC_6:55
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'or' c) = (a '&' ()) 'imp' c
proof end;

theorem :: BVFUNC_6:56
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'imp' b) = a '&' b
proof end;

theorem :: BVFUNC_6:57
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' () = () '&' ()
proof end;

theorem Th12: :: BVFUNC_6:58
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) = ((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)
proof end;

theorem :: BVFUNC_6:59
for Y being non empty set
for a being Function of Y,BOOLEAN holds (I_el Y) 'imp' a = a
proof end;

theorem :: BVFUNC_6:60
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (O_el Y) = 'not' a
proof end;

theorem :: BVFUNC_6:61
for Y being non empty set
for a being Function of Y,BOOLEAN holds (O_el Y) 'imp' a = I_el Y
proof end;

theorem :: BVFUNC_6:62
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (I_el Y) = I_el Y
proof end;

theorem :: BVFUNC_6:63
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' () = 'not' a
proof end;

theorem :: BVFUNC_6:64
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (c 'imp' a) 'imp' (c 'imp' b)
proof end;

theorem :: BVFUNC_6:65
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'eqv' c) 'eqv' (b 'eqv' c)
proof end;

theorem :: BVFUNC_6:66
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'imp' c) 'eqv' (b 'imp' c)
proof end;

theorem :: BVFUNC_6:67
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (c 'imp' a) 'eqv' (c 'imp' b)
proof end;

theorem :: BVFUNC_6:68
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a '&' c) 'eqv' (b '&' c)
proof end;

theorem :: BVFUNC_6:69
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'or' c) 'eqv' (b 'or' c)
proof end;

theorem :: BVFUNC_6:70
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a
proof end;

theorem :: BVFUNC_6:71
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' (a 'imp' b) 'eqv' b
proof end;

theorem :: BVFUNC_6:72
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' (b 'imp' a) 'eqv' a
proof end;

theorem :: BVFUNC_6:73
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a '&' b) 'eqv' (b '&' a)) 'eqv' a
proof end;

theorem :: BVFUNC_6:74
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b '&' c) '&' d) = ((a 'imp' b) '&' (a 'imp' c)) '&' (a 'imp' d)
proof end;

theorem :: BVFUNC_6:75
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b 'or' c) 'or' d) = ((a 'imp' b) 'or' (a 'imp' c)) 'or' (a 'imp' d)
proof end;

theorem :: BVFUNC_6:76
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' d = ((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)
proof end;

theorem :: BVFUNC_6:77
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'or' b) 'or' c) 'imp' d = ((a 'imp' d) '&' (b 'imp' d)) '&' (c 'imp' d)
proof end;

theorem :: BVFUNC_6:78
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (b 'imp' a)) '&' (a 'imp' c)
proof end;

theorem :: BVFUNC_6:79
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a '&' b) 'or' (a '&' ())
proof end;

theorem :: BVFUNC_6:80
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a 'or' b) '&' (a 'or' ())
proof end;

theorem :: BVFUNC_6:81
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a = ((((a '&' b) '&' c) 'or' ((a '&' b) '&' ())) 'or' ((a '&' ()) '&' c)) 'or' ((a '&' ()) '&' ())
proof end;

theorem :: BVFUNC_6:82
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a = ((((a 'or' b) 'or' c) '&' ((a 'or' b) 'or' ())) '&' ((a 'or' ()) 'or' c)) '&' ((a 'or' ()) 'or' ())
proof end;

theorem :: BVFUNC_6:83
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b = a '&' (() 'or' b)
proof end;

theorem :: BVFUNC_6:84
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = a 'or' (() '&' b)
proof end;

theorem :: BVFUNC_6:85
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = 'not' (a 'eqv' b)
proof end;

theorem :: BVFUNC_6:86
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = (a 'or' b) '&' (() 'or' ())
proof end;

theorem :: BVFUNC_6:87
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' (I_el Y) = 'not' a
proof end;

theorem :: BVFUNC_6:88
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' (O_el Y) = a
proof end;

theorem :: BVFUNC_6:89
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = () 'xor' ()
proof end;

theorem :: BVFUNC_6:90
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'xor' b) = a 'xor' ()
proof end;

theorem Th18: :: BVFUNC_6:91
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' ()) '&' (() 'or' b)
proof end;

theorem :: BVFUNC_6:92
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a '&' b) 'or' (() '&' ())
proof end;

theorem :: BVFUNC_6:93
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' (I_el Y) = a
proof end;

theorem :: BVFUNC_6:94
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' (O_el Y) = 'not' a
proof end;

theorem :: BVFUNC_6:95
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'eqv' b) = a 'eqv' ()
proof end;

theorem :: BVFUNC_6:96
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' a '<' (a 'imp' b) 'eqv' ()
proof end;

theorem :: BVFUNC_6:97
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' a '<' (b 'imp' a) 'eqv' ()
proof end;

theorem :: BVFUNC_6:98
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a
proof end;

theorem :: BVFUNC_6:99
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (() 'eqv' ()) = I_el Y
proof end;

theorem :: BVFUNC_6:100
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' a) 'imp' a = I_el Y
proof end;

theorem :: BVFUNC_6:101
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (((a 'imp' c) '&' (b 'imp' d)) '&' (() 'or' ())) 'imp' (() 'or' ()) = I_el Y
proof end;

theorem :: BVFUNC_6:102
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) = I_el Y
proof end;

Lm1: for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a

proof end;

Lm2: for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds
( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b )

proof end;

Lm3: for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b )

proof end;

Lm4: for Y being non empty set
for a, b, c, d, e being Function of Y,BOOLEAN holds
( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b )

proof end;

Lm5: for Y being non empty set
for a, b, c, d, e, f being Function of Y,BOOLEAN holds
( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b )

proof end;

Lm6: for Y being non empty set
for a, b, c, d, e, f, g being Function of Y,BOOLEAN holds
( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b )

proof end;

theorem Th1: :: BVFUNC_6:103
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (b 'imp' c) '<' a 'or' c
proof end;

theorem Th2: :: BVFUNC_6:104
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'imp' b) '<' b
proof end;

theorem :: BVFUNC_6:105
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' () '<' 'not' a
proof end;

theorem :: BVFUNC_6:106
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' () '<' b
proof end;

theorem :: BVFUNC_6:107
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (() 'imp' b) '<' b
proof end;

theorem :: BVFUNC_6:108
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' ()) '<' 'not' a
proof end;

theorem :: BVFUNC_6:109
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b '&' c) '<' a 'imp' b
proof end;

theorem :: BVFUNC_6:110
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'imp' c '<' a 'imp' c
proof end;

theorem :: BVFUNC_6:111
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' b
proof end;

theorem :: BVFUNC_6:112
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' (b '&' c)
proof end;

theorem :: BVFUNC_6:113
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' a 'imp' (b 'or' c)
proof end;

theorem :: BVFUNC_6:114
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a 'or' c) 'imp' (b 'or' c)
proof end;

theorem :: BVFUNC_6:115
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'or' c '<' a 'or' c
proof end;

theorem :: BVFUNC_6:116
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a '&' b) 'or' (c '&' d) '<' a 'or' c
proof end;

theorem :: BVFUNC_6:117
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (() 'imp' c) '<' b 'or' c
proof end;

theorem :: BVFUNC_6:118
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' ()) '<' () 'or' ()
proof end;

theorem :: BVFUNC_6:119
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (() 'or' c) '<' b 'or' c
proof end;

theorem Th918: :: BVFUNC_6:120
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a '&' c) 'imp' (b '&' d)
proof end;

theorem :: BVFUNC_6:121
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c)
proof end;

theorem Th20: :: BVFUNC_6:122
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c
proof end;

theorem Th21: :: BVFUNC_6:123
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a 'or' c) 'imp' (b 'or' d)
proof end;

theorem :: BVFUNC_6:124
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c)
proof end;

theorem Th23: :: BVFUNC_6:125
for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds ((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' a2 'imp' a1
proof end;

Lm7: for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) = I_el Y

proof end;

Lm8: for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (b2 '&' a2))) '&' ('not' (b2 '&' c2))) = I_el Y

proof end;

Lm9: for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) = I_el Y

proof end;

theorem :: BVFUNC_6:126
for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds ((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' ((a2 'imp' a1) '&' (b2 'imp' b1)) '&' (c2 'imp' c1)
proof end;

theorem Th25: :: BVFUNC_6:127
for Y being non empty set
for a1, b1, a2, b2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) 'imp' ('not' (a1 '&' b1)) = I_el Y
proof end;

theorem :: BVFUNC_6:128
for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' (('not' (a1 '&' b1)) '&' ('not' (a1 '&' c1))) '&' ('not' (b1 '&' c1))
proof end;

theorem :: BVFUNC_6:129
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a by Lm1;

theorem :: BVFUNC_6:130
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds
( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b ) by Lm2;

theorem :: BVFUNC_6:131
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b ) by Lm3;

theorem :: BVFUNC_6:132
for Y being non empty set
for a, b, c, d, e being Function of Y,BOOLEAN holds
( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b ) by Lm4;

theorem :: BVFUNC_6:133
for Y being non empty set
for a, b, c, d, e, f being Function of Y,BOOLEAN holds
( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b ) by Lm5;

theorem :: BVFUNC_6:134
for Y being non empty set
for a, b, c, d, e, f, g being Function of Y,BOOLEAN holds
( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b ) by Lm6;

theorem Th33: :: BVFUNC_6:135
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds
a '&' c '<' b '&' d
proof end;

theorem :: BVFUNC_6:136
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '&' () '<' 'not' b
proof end;

theorem :: BVFUNC_6:137
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c
proof end;

theorem :: BVFUNC_6:138
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c
proof end;

theorem :: BVFUNC_6:139
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds
a 'or' c '<' b 'or' d
proof end;

theorem Th38a: :: BVFUNC_6:140
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' a 'or' b
proof end;

theorem :: BVFUNC_6:141
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a 'or' b
proof end;

theorem :: BVFUNC_6:142
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)
proof end;

Lm1: for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' ()) 'or' (b '&' ())) 'or' (c '&' ()) '<' ((b '&' ()) 'or' (c '&' ())) 'or' (a '&' ())

proof end;

theorem :: BVFUNC_6:143
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' ()) 'or' (b '&' ())) 'or' (c '&' ()) = ((b '&' ()) 'or' (c '&' ())) 'or' (a '&' ())
proof end;

Lm2: for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ()) '&' (b 'or' ())) '&' (c 'or' ()) '<' ((b 'or' ()) '&' (c 'or' ())) '&' (a 'or' ())

proof end;

theorem :: BVFUNC_6:144
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ()) '&' (b 'or' ())) '&' (c 'or' ()) = ((b 'or' ()) '&' (c 'or' ())) '&' (a 'or' ())
proof end;

theorem :: BVFUNC_6:145
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds
c 'imp' (a 'or' b) = I_el Y
proof end;

theorem :: BVFUNC_6:146
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds
(a '&' b) 'imp' c = I_el Y
proof end;

theorem :: BVFUNC_6:147
for Y being non empty set
for a1, a2, b1, b2, c1, c2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2
proof end;

Lm3: for Y being non empty set
for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))

proof end;

theorem :: BVFUNC_6:148
for Y being non empty set
for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
proof end;

theorem :: BVFUNC_6:149
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d)
proof end;

theorem :: BVFUNC_6:150
for Y being non empty set
for a1, a2, b1, b2, b3 being Function of Y,BOOLEAN holds (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3)
proof end;

theorem :: BVFUNC_6:151
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d)
proof end;

theorem :: BVFUNC_6:152
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d
proof end;

theorem :: BVFUNC_6:153
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a '&' b) 'imp' ()) '&' a) '&' c '<' 'not' b
proof end;

theorem :: BVFUNC_6:154
for Y being non empty set
for a1, a2, a3, b1, b2, b3 being Function of Y,BOOLEAN holds ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3)
proof end;

theorem :: BVFUNC_6:155
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((() '&' ()) '&' ())
proof end;

theorem :: BVFUNC_6:156
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c
proof end;

Lm4: for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((() '&' b) '&' c) 'or' ((a '&' ()) '&' c)) 'or' ((a '&' b) '&' ()) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c))

proof end;

theorem :: BVFUNC_6:157
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((() '&' b) '&' c) 'or' ((a '&' ()) '&' c)) 'or' ((a '&' b) '&' ())
proof end;

theorem :: BVFUNC_6:158
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b '&' c)
proof end;

theorem :: BVFUNC_6:159
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c
proof end;

theorem Th19: :: BVFUNC_6:160
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' c)
proof end;

theorem Th20: :: BVFUNC_6:161
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ())
proof end;

theorem Th21: :: BVFUNC_6:162
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a)
proof end;

theorem Th22: :: BVFUNC_6:163
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ())
proof end;

theorem :: BVFUNC_6:164
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' b) '&' (b 'imp' (c 'or' a))
proof end;

theorem :: BVFUNC_6:165
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ())) '&' (b 'imp' c)
proof end;

theorem :: BVFUNC_6:166
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c)) '&' (b 'imp' (c 'or' a))
proof end;

theorem :: BVFUNC_6:167
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ())) '&' (b 'imp' (c 'or' a))
proof end;

theorem :: BVFUNC_6:168
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ())) '&' (b 'imp' (c 'or' ()))
proof end;