:: BVFUNC_7 semantic presentation

begin

theorem :: BVFUNC_7:1
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' b) = b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' b) = b
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (('not' a) 'imp' b) = b
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' b) '&' (('not' a) 'imp' b)) . x = b . x
A5: ((a 'imp' b) '&' (('not' a) 'imp' b)) . x = ((a 'imp' b) . x) '&' ((('not' a) 'imp' b) . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' (b . x)) '&' ((('not' a) 'imp' b) . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' (b . x)) '&' (('not' (('not' a) . x)) 'or' (b . x)) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' (b . x)) '&' ((a . x) 'or' (b . x)) by MARGREL1:def_19 ;
now__::_thesis:_(_(_a_._x_=_TRUE_&_((a_'imp'_b)_'&'_(('not'_a)_'imp'_b))_._x_=_b_._x_)_or_(_a_._x_=_FALSE_&_((a_'imp'_b)_'&'_(('not'_a)_'imp'_b))_._x_=_b_._x_)_)
percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3;
case a . x = TRUE ; ::_thesis: ((a 'imp' b) '&' (('not' a) 'imp' b)) . x = b . x
then ((a 'imp' b) '&' (('not' a) 'imp' b)) . x = (FALSE 'or' (b . x)) '&' (TRUE 'or' (b . x)) by A5, MARGREL1:11
.= (FALSE 'or' (b . x)) '&' TRUE by BINARITH:10
.= TRUE '&' (b . x) by BINARITH:3
.= b . x by MARGREL1:14 ;
hence  ((a 'imp' b) '&' (('not' a) 'imp' b)) . x = b . x ; ::_thesis: verum
end;
case a . x = FALSE ; ::_thesis: ((a 'imp' b) '&' (('not' a) 'imp' b)) . x = b . x
then ((a 'imp' b) '&' (('not' a) 'imp' b)) . x = (TRUE 'or' (b . x)) '&' (FALSE 'or' (b . x)) by A5, MARGREL1:11
.= TRUE '&' (FALSE 'or' (b . x)) by BINARITH:10
.= TRUE '&' (b . x) by BINARITH:3
.= b . x by MARGREL1:14 ;
hence  ((a 'imp' b) '&' (('not' a) 'imp' b)) . x = b . x ; ::_thesis: verum
end;
end;
end;
hence  ((a 'imp' b) '&' (('not' a) 'imp' b)) . x = b . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:2
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' ('not' b)) = 'not' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' ('not' b)) = 'not' a
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (a 'imp' ('not' b)) = 'not' a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' b) '&' (a 'imp' ('not' b))) . x = ('not' a) . x
A5: ((a 'imp' b) '&' (a 'imp' ('not' b))) . x = ((a 'imp' b) . x) '&' ((a 'imp' ('not' b)) . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' (b . x)) '&' ((a 'imp' ('not' b)) . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' (b . x)) '&' (('not' (a . x)) 'or' (('not' b) . x)) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' (b . x)) '&' (('not' (a . x)) 'or' ('not' (b . x))) by MARGREL1:def_19 ;
now__::_thesis:_(_(_b_._x_=_TRUE_&_((a_'imp'_b)_'&'_(a_'imp'_('not'_b)))_._x_=_('not'_a)_._x_)_or_(_b_._x_=_FALSE_&_((a_'imp'_b)_'&'_(a_'imp'_('not'_b)))_._x_=_('not'_a)_._x_)_)
percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3;
case b . x = TRUE ; ::_thesis: ((a 'imp' b) '&' (a 'imp' ('not' b))) . x = ('not' a) . x
then ((a 'imp' b) '&' (a 'imp' ('not' b))) . x = (('not' (a . x)) 'or' TRUE) '&' (('not' (a . x)) 'or' FALSE) by A5, MARGREL1:11
.= (('not' (a . x)) 'or' TRUE) '&' ('not' (a . x)) by BINARITH:3
.= TRUE '&' ('not' (a . x)) by BINARITH:10
.= 'not' (a . x) by MARGREL1:14
.= ('not' a) . x by MARGREL1:def_19 ;
hence  ((a 'imp' b) '&' (a 'imp' ('not' b))) . x = ('not' a) . x ; ::_thesis: verum
end;
case b . x = FALSE ; ::_thesis: ((a 'imp' b) '&' (a 'imp' ('not' b))) . x = ('not' a) . x
then ((a 'imp' b) '&' (a 'imp' ('not' b))) . x = (('not' (a . x)) 'or' FALSE) '&' (('not' (a . x)) 'or' TRUE) by A5, MARGREL1:11
.= ('not' (a . x)) '&' (('not' (a . x)) 'or' TRUE) by BINARITH:3
.= TRUE '&' ('not' (a . x)) by BINARITH:10
.= 'not' (a . x) by MARGREL1:14
.= ('not' a) . x by MARGREL1:def_19 ;
hence  ((a 'imp' b) '&' (a 'imp' ('not' b))) . x = ('not' a) . x ; ::_thesis: verum
end;
end;
end;
hence  ((a 'imp' b) '&' (a 'imp' ('not' b))) . x = ('not' a) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:3
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'or' c) = (a 'imp' b) 'or' (a 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b 'or' c) = (a 'imp' b) 'or' (a 'imp' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' (b 'or' c)) . x = ((a 'imp' b) 'or' (a 'imp' c)) . x
((a 'imp' b) 'or' (a 'imp' c)) . x = ((a 'imp' b) . x) 'or' ((a 'imp' c) . x) by BVFUNC_1:def_4
.= (('not' (a . x)) 'or' (b . x)) 'or' ((a 'imp' c) . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' (b . x)) 'or' (('not' (a . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' (('not' (a . x)) 'or' (b . x))) 'or' (c . x) by BINARITH:11
.= ((('not' (a . x)) 'or' ('not' (a . x))) 'or' (b . x)) 'or' (c . x) by BINARITH:11
.= ('not' (a . x)) 'or' ((b . x) 'or' (c . x)) by BINARITH:11
.= ('not' (a . x)) 'or' ((b 'or' c) . x) by BVFUNC_1:def_4
.= (a 'imp' (b 'or' c)) . x by BVFUNC_1:def_8 ;
hence  (a 'imp' (b 'or' c)) . x = ((a 'imp' b) 'or' (a 'imp' c)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:4
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b '&' c) = (a 'imp' b) '&' (a 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b '&' c) = (a 'imp' b) '&' (a 'imp' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' (b '&' c)) . x = ((a 'imp' b) '&' (a 'imp' c)) . x
((a 'imp' b) '&' (a 'imp' c)) . x = ((a 'imp' b) . x) '&' ((a 'imp' c) . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' (b . x)) '&' ((a 'imp' c) . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' (b . x)) '&' (('not' (a . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' ((b . x) '&' (c . x)) by XBOOLEAN:9
.= ('not' (a . x)) 'or' ((b '&' c) . x) by MARGREL1:def_20
.= (a 'imp' (b '&' c)) . x by BVFUNC_1:def_8 ;
hence  (a 'imp' (b '&' c)) . x = ((a 'imp' b) '&' (a 'imp' c)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:5
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'imp' c = (a 'imp' c) '&' (b 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) 'imp' c = (a 'imp' c) '&' (b 'imp' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'or' b) 'imp' c) . x = ((a 'imp' c) '&' (b 'imp' c)) . x
((a 'imp' c) '&' (b 'imp' c)) . x = ((a 'imp' c) . x) '&' ((b 'imp' c) . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' (c . x)) '&' ((b 'imp' c) . x) by BVFUNC_1:def_8
.= ((c . x) 'or' ('not' (a . x))) '&' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= ('not' ((a . x) 'or' (b . x))) 'or' (c . x) by XBOOLEAN:9
.= ('not' ((a 'or' b) . x)) 'or' (c . x) by BVFUNC_1:def_4
.= ((a 'or' b) 'imp' c) . x by BVFUNC_1:def_8 ;
hence  ((a 'or' b) 'imp' c) . x = ((a 'imp' c) '&' (b 'imp' c)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:6
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = (a 'imp' c) 'or' (b 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'imp' c = (a 'imp' c) 'or' (b 'imp' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a '&' b) 'imp' c) . x = ((a 'imp' c) 'or' (b 'imp' c)) . x
((a 'imp' c) 'or' (b 'imp' c)) . x = ((a 'imp' c) . x) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_4
.= (('not' (a . x)) 'or' (c . x)) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' (c . x)) 'or' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ((c . x) 'or' ('not' (b . x)))) 'or' (c . x) by BINARITH:11
.= ((('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x)) 'or' (c . x) by BINARITH:11
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' ((c . x) 'or' (c . x)) by BINARITH:11
.= ('not' ((a '&' b) . x)) 'or' (c . x) by MARGREL1:def_20
.= ((a '&' b) 'imp' c) . x by BVFUNC_1:def_8 ;
hence  ((a '&' b) 'imp' c) . x = ((a 'imp' c) 'or' (b 'imp' c)) . x ; ::_thesis: verum
end;

theorem Th7: :: BVFUNC_7:7
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = a 'imp' (b 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'imp' c = a 'imp' (b 'imp' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a '&' b) 'imp' c) . x = (a 'imp' (b 'imp' c)) . x
(a 'imp' (b 'imp' c)) . x = ('not' (a . x)) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x) by BINARITH:11
.= ('not' ((a '&' b) . x)) 'or' (c . x) by MARGREL1:def_20
.= ((a '&' b) 'imp' c) . x by BVFUNC_1:def_8 ;
hence  ((a '&' b) 'imp' c) . x = (a 'imp' (b 'imp' c)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = a 'imp' (('not' b) 'or' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = a 'imp' (('not' b) 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'imp' c = a 'imp' (('not' b) 'or' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a '&' b) 'imp' c) . x = (a 'imp' (('not' b) 'or' c)) . x
 (a 'imp' (('not' b) 'or' c)) . x = (a 'imp' (b 'imp' c)) . x by BVFUNC_4:8;
hence  ((a '&' b) 'imp' c) . x = (a 'imp' (('not' b) 'or' c)) . x by Th7; ::_thesis: verum
end;

theorem :: BVFUNC_7:9
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'or' c) = (a '&' ('not' b)) 'imp' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'or' c) = (a '&' ('not' b)) 'imp' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b 'or' c) = (a '&' ('not' b)) 'imp' c
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' (b 'or' c)) . x = ((a '&' ('not' b)) 'imp' c) . x
((a '&' ('not' b)) 'imp' c) . x = ('not' ((a '&' ('not' b)) . x)) 'or' (c . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (('not' b) . x))) 'or' (c . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' (b . x)) 'or' (c . x) by MARGREL1:def_19
.= ('not' (a . x)) 'or' ((b . x) 'or' (c . x)) by BINARITH:11
.= ('not' (a . x)) 'or' ((b 'or' c) . x) by BVFUNC_1:def_4
.= (a 'imp' (b 'or' c)) . x by BVFUNC_1:def_8 ;
hence  (a 'imp' (b 'or' c)) . x = ((a '&' ('not' b)) 'imp' c) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'imp' b) = a '&' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' (a 'imp' b) = a '&' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' (a 'imp' b) = a '&' b
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a '&' (a 'imp' b)) . x = (a '&' b) . x
(a '&' (a 'imp' b)) . x = (a . x) '&' ((a 'imp' b) . x) by MARGREL1:def_20
.= (a . x) '&' (('not' (a . x)) 'or' (b . x)) by BVFUNC_1:def_8
.= ((a . x) '&' ('not' (a . x))) 'or' ((a . x) '&' (b . x)) by XBOOLEAN:8
.= FALSE 'or' ((a . x) '&' (b . x)) by XBOOLEAN:138
.= (a . x) '&' (b . x) by BINARITH:3
.= (a '&' b) . x by MARGREL1:def_20 ;
hence  (a '&' (a 'imp' b)) . x = (a '&' b) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:11
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' ('not' b) = ('not' a) '&' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' ('not' b) = ('not' a) '&' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' ('not' b) = ('not' a) '&' ('not' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' b) '&' ('not' b)) . x = (('not' a) '&' ('not' b)) . x
((a 'imp' b) '&' ('not' b)) . x = ((a 'imp' b) . x) '&' (('not' b) . x) by MARGREL1:def_20
.= (('not' b) . x) '&' (('not' (a . x)) 'or' (b . x)) by BVFUNC_1:def_8
.= ((('not' b) . x) '&' ('not' (a . x))) 'or' ((('not' b) . x) '&' (b . x)) by XBOOLEAN:8
.= ((('not' b) . x) '&' ('not' (a . x))) 'or' ((b . x) '&' ('not' (b . x))) by MARGREL1:def_19
.= ((('not' b) . x) '&' ('not' (a . x))) 'or' FALSE by XBOOLEAN:138
.= (('not' b) . x) '&' ('not' (a . x)) by BINARITH:3
.= (('not' b) . x) '&' (('not' a) . x) by MARGREL1:def_19
.= (('not' a) '&' ('not' b)) . x by MARGREL1:def_20 ;
hence  ((a 'imp' b) '&' ('not' b)) . x = (('not' a) '&' ('not' b)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:12
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
let Y be non empty set ; ::_thesis: 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)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) = ((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x
A5: (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) . x) '&' ((a 'imp' c) . x) by MARGREL1:def_20
.= (((a 'imp' b) . x) '&' ((b 'imp' c) . x)) '&' ((a 'imp' c) . x) by MARGREL1:def_20
.= ((('not' (a . x)) 'or' (b . x)) '&' ((b 'imp' c) . x)) '&' ((a 'imp' c) . x) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' ((a 'imp' c) . x) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' (('not' (a . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= (((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' ('not' (a . x))) 'or' (((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' (c . x)) by XBOOLEAN:8 ;
A6: (('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x)) = ((a 'imp' b) . x) '&' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= ((a 'imp' b) . x) '&' ((b 'imp' c) . x) by BVFUNC_1:def_8
.= ((a 'imp' b) '&' (b 'imp' c)) . x by MARGREL1:def_20 ;
A7: ((a 'imp' b) '&' (b 'imp' c)) . x = ((a 'imp' b) . x) '&' ((b 'imp' c) . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' (b . x)) '&' ((b 'imp' c) . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8 ;
now__::_thesis:_(_(_a_._x_=_TRUE_&_c_._x_=_TRUE_&_((a_'imp'_b)_'&'_(b_'imp'_c))_._x_=_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(a_'imp'_c))_._x_)_or_(_a_._x_=_TRUE_&_c_._x_=_FALSE_&_((a_'imp'_b)_'&'_(b_'imp'_c))_._x_=_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(a_'imp'_c))_._x_)_or_(_a_._x_=_FALSE_&_c_._x_=_TRUE_&_((a_'imp'_b)_'&'_(b_'imp'_c))_._x_=_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(a_'imp'_c))_._x_)_or_(_a_._x_=_FALSE_&_c_._x_=_FALSE_&_((a_'imp'_b)_'&'_(b_'imp'_c))_._x_=_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(a_'imp'_c))_._x_)_)
percases ( ( a . x = TRUE & c . x = TRUE ) or ( a . x = TRUE & c . x = FALSE ) or ( a . x = FALSE & c . x = TRUE ) or ( a . x = FALSE & c . x = FALSE ) ) by XBOOLEAN:def_3;
case ( a . x = TRUE & c . x = TRUE ) ; ::_thesis: ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x
then (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x = (((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' FALSE) 'or' (((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' TRUE) by A5, MARGREL1:11
.= FALSE 'or' (((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' TRUE) by MARGREL1:13
.= FALSE 'or' ((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) by MARGREL1:14
.= ((a 'imp' b) '&' (b 'imp' c)) . x by A6, BINARITH:3 ;
hence  ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x ; ::_thesis: verum
end;
caseA8: ( a . x = TRUE & c . x = FALSE ) ; ::_thesis: ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x
then A9: ((a 'imp' b) '&' (b 'imp' c)) . x = (FALSE 'or' (b . x)) '&' (('not' (b . x)) 'or' FALSE) by A7, MARGREL1:11
.= (FALSE 'or' (b . x)) '&' ('not' (b . x)) by BINARITH:3
.= (b . x) '&' ('not' (b . x)) by BINARITH:3
.= FALSE by XBOOLEAN:138 ;
(((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x = (((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' FALSE) 'or' (((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' FALSE) by A5, A8, MARGREL1:11
.= FALSE by MARGREL1:13 ;
hence  ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x by A9; ::_thesis: verum
end;
case ( a . x = FALSE & c . x = TRUE ) ; ::_thesis: ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x
then (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x = (((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' TRUE) 'or' (((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) '&' TRUE) by A5, MARGREL1:11
.= ((a 'imp' b) '&' (b 'imp' c)) . x by A6, MARGREL1:14 ;
hence  ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x ; ::_thesis: verum
end;
case ( a . x = FALSE & c . x = FALSE ) ; ::_thesis: ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x
then (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x = (TRUE '&' ((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x)))) 'or' (FALSE '&' ((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x)))) by A5, MARGREL1:11
.= ((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) 'or' (FALSE '&' ((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x)))) by MARGREL1:14
.= ((('not' (a . x)) 'or' (b . x)) '&' (('not' (b . x)) 'or' (c . x))) 'or' FALSE by MARGREL1:13
.= ((a 'imp' b) '&' (b 'imp' c)) . x by A6, BINARITH:3 ;
hence  ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x ; ::_thesis: verum
end;
end;
end;
hence  ((a 'imp' b) '&' (b 'imp' c)) . x = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:13
for Y being non empty set
for a being Function of Y,BOOLEAN holds (I_el Y) 'imp' a = a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (I_el Y) 'imp' a = a
let a be Function of Y,BOOLEAN; ::_thesis: (I_el Y) 'imp' a = a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((I_el Y) 'imp' a) . x = a . x
((I_el Y) 'imp' a) . x = ('not' ((I_el Y) . x)) 'or' (a . x) by BVFUNC_1:def_8
.= FALSE 'or' (a . x) by MARGREL1:11, BVFUNC_1:def_11 ;
hence  ((I_el Y) 'imp' a) . x = a . x by BINARITH:3; ::_thesis: verum
end;

theorem :: BVFUNC_7:14
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (O_el Y) = 'not' a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'imp' (O_el Y) = 'not' a
let a be Function of Y,BOOLEAN; ::_thesis: a 'imp' (O_el Y) = 'not' a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' (O_el Y)) . x = ('not' a) . x
(a 'imp' (O_el Y)) . x = ('not' (a . x)) 'or' ((O_el Y) . x) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' FALSE by BVFUNC_1:def_10
.= 'not' (a . x) by BINARITH:3 ;
hence  (a 'imp' (O_el Y)) . x = ('not' a) . x by MARGREL1:def_19; ::_thesis: verum
end;

theorem :: BVFUNC_7:15
for Y being non empty set
for a being Function of Y,BOOLEAN holds (O_el Y) 'imp' a = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (O_el Y) 'imp' a = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: (O_el Y) 'imp' a = I_el Y
 for x being Element of Y holds ((O_el Y) 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((O_el Y) 'imp' a) . x = TRUE
((O_el Y) 'imp' a) . x = ('not' ((O_el Y) . x)) 'or' (a . x) by BVFUNC_1:def_8
.= TRUE 'or' (a . x) by MARGREL1:11, BVFUNC_1:def_10 ;
hence  ((O_el Y) 'imp' a) . x = TRUE by BINARITH:10; ::_thesis: verum
end;
hence  (O_el Y) 'imp' a = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_7:16
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (I_el Y) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'imp' (I_el Y) = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a 'imp' (I_el Y) = I_el Y
 for x being Element of Y holds (a 'imp' (I_el Y)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' (I_el Y)) . x = TRUE
(a 'imp' (I_el Y)) . x = ('not' (a . x)) 'or' ((I_el Y) . x) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' TRUE by BVFUNC_1:def_11 ;
hence  (a 'imp' (I_el Y)) . x = TRUE by BINARITH:10; ::_thesis: verum
end;
hence  a 'imp' (I_el Y) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_7:17
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' ('not' a) = 'not' a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'imp' ('not' a) = 'not' a
let a be Function of Y,BOOLEAN; ::_thesis: a 'imp' ('not' a) = 'not' a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' ('not' a)) . x = ('not' a) . x
(a 'imp' ('not' a)) . x = ('not' (a . x)) 'or' (('not' a) . x) by BVFUNC_1:def_8
.= (('not' a) . x) 'or' (('not' a) . x) by MARGREL1:def_19
.= ('not' a) . x ;
hence  (a 'imp' ('not' a)) . x = ('not' a) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_7:18
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (c 'imp' a) 'imp' (c 'imp' b)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' b '<' (c 'imp' a) 'imp' (c 'imp' b)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'imp' b) . z = TRUE or ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE )
assume  (a 'imp' b) . z = TRUE ; ::_thesis: ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE
then A1: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def_8;
A2: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_(a_._z)_=_TRUE_&_((c_'imp'_a)_'imp'_(c_'imp'_b))_._z_=_TRUE_)_or_(_b_._z_=_TRUE_&_((c_'imp'_a)_'imp'_(c_'imp'_b))_._z_=_TRUE_)_)
percases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A1, A2, BINARITH:3;
caseA3: 'not' (a . z) = TRUE ; ::_thesis: ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE
((c 'imp' a) 'imp' (c 'imp' b)) . z = ('not' ((c 'imp' a) . z)) 'or' ((c 'imp' b) . z) by BVFUNC_1:def_8
.= ('not' (('not' (c . z)) 'or' (a . z))) 'or' ((c 'imp' b) . z) by BVFUNC_1:def_8
.= (c . z) 'or' ((c 'imp' b) . z) by A3, MARGREL1:14
.= (c . z) 'or' (('not' (c . z)) 'or' (b . z)) by BVFUNC_1:def_8
.= ((c . z) 'or' ('not' (c . z))) 'or' (b . z) by BINARITH:11
.= TRUE 'or' (b . z) by XBOOLEAN:102
.= TRUE by BINARITH:10 ;
hence  ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE ; ::_thesis: verum
end;
caseA4: b . z = TRUE ; ::_thesis: ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE
((c 'imp' a) 'imp' (c 'imp' b)) . z = ('not' ((c 'imp' a) . z)) 'or' ((c 'imp' b) . z) by BVFUNC_1:def_8
.= ('not' (('not' (c . z)) 'or' (a . z))) 'or' ((c 'imp' b) . z) by BVFUNC_1:def_8
.= ('not' (('not' (c . z)) 'or' (a . z))) 'or' (('not' (c . z)) 'or' TRUE) by A4, BVFUNC_1:def_8
.= ('not' (('not' (c . z)) 'or' (a . z))) 'or' TRUE by BINARITH:10
.= TRUE by BINARITH:10 ;
hence  ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_7:19
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'eqv' c) 'eqv' (b 'eqv' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b '<' (a 'eqv' c) 'eqv' (b 'eqv' c)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'eqv' b) . z = TRUE or ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE )
A1: (a 'eqv' b) . z = ((a 'imp' b) '&' (b 'imp' a)) . z by BVFUNC_4:7
.= ((a 'imp' b) . z) '&' ((b 'imp' a) . z) by MARGREL1:def_20 ;
assume A2: (a 'eqv' b) . z = TRUE ; ::_thesis: ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE
then  (a 'imp' b) . z = TRUE by A1, MARGREL1:12;
then A3: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def_8;
A4: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3;
A5: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
A6: (b 'imp' a) . z = ('not' (b . z)) 'or' (a . z) by BVFUNC_1:def_8;
A7: ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = (((a 'eqv' c) 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' (a 'eqv' c))) . z by BVFUNC_4:7
.= ((((a 'imp' c) '&' (c 'imp' a)) 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' (a 'eqv' c))) . z by BVFUNC_4:7
.= ((((a 'imp' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' ((b 'eqv' c) 'imp' (a 'eqv' c))) . z by BVFUNC_4:7
.= ((((a 'imp' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' (a 'eqv' c))) . z by BVFUNC_4:7
.= ((((a 'imp' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:7
.= ((((('not' a) 'or' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' ((('not' a) 'or' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_4:8
.= ((('not' ((('not' a) 'or' c) '&' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_4:8
.= ((('not' ((('not' a) 'or' c) '&' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (('not' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_4:8
.= (((('not' (('not' a) 'or' c)) 'or' ('not' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (('not' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:14
.= (((('not' (('not' a) 'or' c)) 'or' ('not' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' ((('not' (('not' b) 'or' c)) 'or' ('not' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:14
.= ((((('not' ('not' a)) '&' ('not' c)) 'or' ('not' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' ((('not' (('not' b) 'or' c)) 'or' ('not' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:13
.= ((((('not' ('not' a)) '&' ('not' c)) 'or' (('not' ('not' c)) '&' ('not' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' ((('not' (('not' b) 'or' c)) 'or' ('not' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:13
.= ((((('not' ('not' a)) '&' ('not' c)) 'or' (('not' ('not' c)) '&' ('not' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' ('not' b)) '&' ('not' c)) 'or' ('not' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:13
.= ((((a '&' ('not' c)) 'or' (c '&' ('not' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b '&' ('not' c)) 'or' (('not' ('not' c)) '&' ('not' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:13
.= ((((a '&' ('not' c)) 'or' (c '&' ('not' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) . z) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a))) . z) by MARGREL1:def_20
.= ((((a '&' ('not' c)) 'or' (c '&' ('not' a))) . z) 'or' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) . z)) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a))) . z) by BVFUNC_1:def_4
.= ((((a '&' ('not' c)) 'or' (c '&' ('not' a))) . z) 'or' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) . z)) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) . z) 'or' (((('not' a) 'or' c) '&' (('not' c) 'or' a)) . z)) by BVFUNC_1:def_4
.= ((((a '&' ('not' c)) . z) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) . z)) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) . z) 'or' (((('not' a) 'or' c) '&' (('not' c) 'or' a)) . z)) by BVFUNC_1:def_4
.= ((((a '&' ('not' c)) . z) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) . z) 'or' (((('not' a) 'or' c) '&' (('not' c) 'or' a)) . z)) by MARGREL1:def_20
.= ((((a '&' ('not' c)) . z) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) '&' (('not' c) 'or' a)) . z)) by BVFUNC_1:def_4
.= ((((a '&' ('not' c)) . z) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def_20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def_20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def_20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by BVFUNC_1:def_4
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by BVFUNC_1:def_4
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def_20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def_20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) 'or' a) . z))) by BVFUNC_1:def_4
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by BVFUNC_1:def_4
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (a . z)))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by MARGREL1:def_19
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (a . z)))) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by MARGREL1:def_19
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (a . z)))) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by MARGREL1:def_19
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (a . z)))) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((('not' (a . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by MARGREL1:def_19 ;
 (b 'imp' a) . z = TRUE by A2, A1, MARGREL1:12;
then A8: ( 'not' (b . z) = TRUE or a . z = TRUE ) by A6, A4, BINARITH:3;
now__::_thesis:_(_(_'not'_(a_._z)_=_TRUE_&_((a_'eqv'_c)_'eqv'_(b_'eqv'_c))_._z_=_TRUE_)_or_(_b_._z_=_TRUE_&_((a_'eqv'_c)_'eqv'_(b_'eqv'_c))_._z_=_TRUE_)_)
percases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A3, A5, BINARITH:3;
caseA9: 'not' (a . z) = TRUE ; ::_thesis: ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE
then  a . z = FALSE by MARGREL1:11;
then ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = ((FALSE 'or' ((c . z) '&' TRUE)) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((TRUE 'or' (c . z)) '&' ((('not' c) . z) 'or' FALSE))) by A7, A9, MARGREL1:13
.= ((FALSE 'or' (c . z)) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((TRUE 'or' (c . z)) '&' ((('not' c) . z) 'or' FALSE))) by MARGREL1:14
.= ((c . z) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((TRUE 'or' (c . z)) '&' ((('not' c) . z) 'or' FALSE))) by BINARITH:3
.= ((c . z) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((TRUE 'or' (c . z)) '&' (('not' c) . z))) by BINARITH:3
.= ((c . z) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (TRUE '&' (('not' c) . z))) by BINARITH:10
.= ((c . z) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by MARGREL1:14
.= (((c . z) 'or' ((c . z) 'or' ('not' (b . z)))) '&' ((c . z) 'or' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by XBOOLEAN:9
.= ((((c . z) 'or' (c . z)) 'or' ('not' (b . z))) '&' ((c . z) 'or' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by BINARITH:11
.= (((c . z) 'or' ('not' (b . z))) '&' (((c . z) 'or' (('not' c) . z)) 'or' (b . z))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by BINARITH:11
.= (((c . z) 'or' ('not' (b . z))) '&' (((c . z) 'or' ('not' (c . z))) 'or' (b . z))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by MARGREL1:def_19
.= (((c . z) 'or' ('not' (b . z))) '&' (TRUE 'or' (b . z))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by XBOOLEAN:102
.= (TRUE '&' ((c . z) 'or' ('not' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by BINARITH:10
.= ((c . z) 'or' ('not' (b . z))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by MARGREL1:14
.= ((c . z) 'or' ('not' (b . z))) '&' (((b . z) '&' (('not' c) . z)) 'or' ((('not' c) . z) 'or' ((c . z) '&' ('not' (b . z))))) by BINARITH:11
.= ((c . z) 'or' ('not' (b . z))) '&' (((b . z) '&' (('not' c) . z)) 'or' (((('not' c) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' ('not' (b . z))))) by XBOOLEAN:9
.= ((c . z) 'or' ('not' (b . z))) '&' (((b . z) '&' (('not' c) . z)) 'or' ((('not' (c . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' ('not' (b . z))))) by MARGREL1:def_19
.= ((c . z) 'or' ('not' (b . z))) '&' (((b . z) '&' (('not' c) . z)) 'or' (TRUE '&' ((('not' c) . z) 'or' ('not' (b . z))))) by XBOOLEAN:102
.= ((c . z) 'or' ('not' (b . z))) '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' ((b . z) '&' (('not' c) . z))) by MARGREL1:14
.= ((c . z) 'or' ('not' (b . z))) '&' ((((('not' c) . z) 'or' ('not' (b . z))) 'or' (b . z)) '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' (('not' c) . z))) by XBOOLEAN:9
.= ((c . z) 'or' ('not' (b . z))) '&' (((('not' c) . z) 'or' (('not' (b . z)) 'or' (b . z))) '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' (('not' c) . z))) by BINARITH:11
.= ((c . z) 'or' ('not' (b . z))) '&' (((('not' c) . z) 'or' TRUE) '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' (('not' c) . z))) by XBOOLEAN:102
.= ((c . z) 'or' ('not' (b . z))) '&' (TRUE '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' (('not' c) . z))) by BINARITH:10
.= ((c . z) 'or' ('not' (b . z))) '&' ((('not' (b . z)) 'or' (('not' c) . z)) 'or' (('not' c) . z)) by MARGREL1:14
.= ((c . z) 'or' ('not' (b . z))) '&' (('not' (b . z)) 'or' ((('not' c) . z) 'or' (('not' c) . z))) by BINARITH:11
.= (('not' (b . z)) '&' ((c . z) 'or' ('not' (b . z)))) 'or' (((c . z) 'or' ('not' (b . z))) '&' (('not' c) . z)) by XBOOLEAN:8
.= ((('not' (b . z)) '&' (c . z)) 'or' (('not' (b . z)) '&' ('not' (b . z)))) 'or' ((('not' c) . z) '&' ((c . z) 'or' ('not' (b . z)))) by XBOOLEAN:8
.= ((('not' (b . z)) '&' (c . z)) 'or' ('not' (b . z))) 'or' (((('not' c) . z) '&' (c . z)) 'or' ((('not' c) . z) '&' ('not' (b . z)))) by XBOOLEAN:8
.= ((('not' (b . z)) '&' (c . z)) 'or' ('not' (b . z))) 'or' (((c . z) '&' ('not' (c . z))) 'or' ((('not' c) . z) '&' ('not' (b . z)))) by MARGREL1:def_19
.= ((('not' (b . z)) '&' (c . z)) 'or' ('not' (b . z))) 'or' (FALSE 'or' ((('not' c) . z) '&' ('not' (b . z)))) by XBOOLEAN:138
.= (('not' (b . z)) 'or' (('not' (b . z)) '&' (c . z))) 'or' ((('not' c) . z) '&' ('not' (b . z))) by BINARITH:3
.= ('not' (b . z)) 'or' ((('not' (b . z)) '&' (c . z)) 'or' ((('not' c) . z) '&' ('not' (b . z)))) by BINARITH:11
.= TRUE by A8, A9, BINARITH:10, MARGREL1:11 ;
hence  ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE ; ::_thesis: verum
end;
caseA10: b . z = TRUE ; ::_thesis: ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE
then  'not' (b . z) = FALSE by MARGREL1:11;
then ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = (((('not' c) . z) 'or' (FALSE '&' (c . z))) 'or' ((FALSE 'or' (c . z)) '&' ((('not' c) . z) 'or' TRUE))) '&' (((('not' c) . z) 'or' ((c . z) '&' FALSE)) 'or' ((FALSE 'or' (c . z)) '&' ((('not' c) . z) 'or' TRUE))) by A2, A1, A6, A4, A7, A10, MARGREL1:12, MARGREL1:14
.= (((('not' c) . z) 'or' FALSE) 'or' ((FALSE 'or' (c . z)) '&' ((('not' c) . z) 'or' TRUE))) '&' (((('not' c) . z) 'or' FALSE) 'or' ((FALSE 'or' (c . z)) '&' ((('not' c) . z) 'or' TRUE))) by MARGREL1:13
.= (((('not' c) . z) 'or' FALSE) 'or' ((FALSE 'or' (c . z)) '&' TRUE)) '&' (((('not' c) . z) 'or' FALSE) 'or' ((FALSE 'or' (c . z)) '&' TRUE)) by BINARITH:10
.= (((('not' c) . z) 'or' FALSE) 'or' ((c . z) '&' TRUE)) '&' (((('not' c) . z) 'or' FALSE) 'or' ((c . z) '&' TRUE)) by BINARITH:3
.= ((('not' c) . z) 'or' (TRUE '&' (c . z))) '&' ((('not' c) . z) 'or' ((c . z) '&' TRUE)) by BINARITH:3
.= ((('not' c) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (c . z)) by MARGREL1:14
.= (('not' (c . z)) 'or' (c . z)) '&' (('not' (c . z)) 'or' (c . z)) by MARGREL1:def_19
.= TRUE by XBOOLEAN:102 ;
hence  ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_7:20
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'imp' c) 'eqv' (b 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b '<' (a 'imp' c) 'eqv' (b 'imp' c)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'eqv' b) . z = TRUE or ((a 'imp' c) 'eqv' (b 'imp' c)) . z = TRUE )
A1: (a 'eqv' b) . z = ((a 'imp' b) '&' (b 'imp' a)) . z by BVFUNC_4:7
.= ((a 'imp' b) . z) '&' ((b 'imp' a) . z) by MARGREL1:def_20 ;
assume A2: (a 'eqv' b) . z = TRUE ; ::_thesis: ((a 'imp' c) 'eqv' (b 'imp' c)) . z = TRUE
then  (a 'imp' b) . z = TRUE by A1, MARGREL1:12;
then A3: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def_8;
 (b 'imp' a) . z = TRUE by A2, A1, MARGREL1:12;
then A4: ('not' (b . z)) 'or' (a . z) = TRUE by BVFUNC_1:def_8;
A5: ((a 'imp' c) 'eqv' (b 'imp' c)) . z = (((a 'imp' c) 'imp' (b 'imp' c)) '&' ((b 'imp' c) 'imp' (a 'imp' c))) . z by BVFUNC_4:7
.= (((a 'imp' c) 'imp' (b 'imp' c)) . z) '&' (((b 'imp' c) 'imp' (a 'imp' c)) . z) by MARGREL1:def_20
.= (('not' ((a 'imp' c) . z)) 'or' ((b 'imp' c) . z)) '&' (((b 'imp' c) 'imp' (a 'imp' c)) . z) by BVFUNC_1:def_8
.= (('not' ((a 'imp' c) . z)) 'or' ((b 'imp' c) . z)) '&' (('not' ((b 'imp' c) . z)) 'or' ((a 'imp' c) . z)) by BVFUNC_1:def_8
.= (('not' (('not' (a . z)) 'or' (c . z))) 'or' ((b 'imp' c) . z)) '&' (('not' ((b 'imp' c) . z)) 'or' ((a 'imp' c) . z)) by BVFUNC_1:def_8
.= (('not' (('not' (a . z)) 'or' (c . z))) 'or' (('not' (b . z)) 'or' (c . z))) '&' (('not' ((b 'imp' c) . z)) 'or' ((a 'imp' c) . z)) by BVFUNC_1:def_8
.= (('not' (('not' (a . z)) 'or' (c . z))) 'or' (('not' (b . z)) 'or' (c . z))) '&' (('not' (('not' (b . z)) 'or' (c . z))) 'or' ((a 'imp' c) . z)) by BVFUNC_1:def_8
.= (((a . z) '&' ('not' (c . z))) 'or' (('not' (b . z)) 'or' (c . z))) '&' (((b . z) '&' ('not' (c . z))) 'or' (('not' (a . z)) 'or' (c . z))) by BVFUNC_1:def_8 ;
A6: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3;
A7: (b 'imp' a) . z = ('not' (b . z)) 'or' (a . z) by BVFUNC_1:def_8;
A8: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_(a_._z)_=_TRUE_&_((a_'imp'_c)_'eqv'_(b_'imp'_c))_._z_=_TRUE_)_or_(_b_._z_=_TRUE_&_((a_'imp'_c)_'eqv'_(b_'imp'_c))_._z_=_TRUE_)_)
percases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A3, A8, BINARITH:3;
caseA9: 'not' (a . z) = TRUE ; ::_thesis: ((a 'imp' c) 'eqv' (b 'imp' c)) . z = TRUE
then A10: a . z = FALSE by MARGREL1:11;
then  'not' (b . z) = TRUE by A4, BINARITH:3;
then ((a 'imp' c) 'eqv' (b 'imp' c)) . z = (FALSE 'or' (TRUE 'or' (c . z))) '&' (FALSE 'or' (TRUE 'or' (c . z))) by A5, A9, A10, MARGREL1:13
.= (TRUE 'or' (c . z)) '&' (TRUE 'or' (c . z)) by BINARITH:3
.= TRUE by BINARITH:10 ;
hence  ((a 'imp' c) 'eqv' (b 'imp' c)) . z = TRUE ; ::_thesis: verum
end;
caseA11: b . z = TRUE ; ::_thesis: ((a 'imp' c) 'eqv' (b 'imp' c)) . z = TRUE
then  'not' (b . z) = FALSE by MARGREL1:11;
then ((a 'imp' c) 'eqv' (b 'imp' c)) . z = (('not' (c . z)) 'or' (FALSE 'or' (c . z))) '&' (('not' (c . z)) 'or' (FALSE 'or' (c . z))) by A2, A1, A7, A6, A5, A11, BINARITH:3, MARGREL1:12
.= (('not' (c . z)) 'or' (c . z)) '&' (('not' (c . z)) 'or' (c . z)) by BINARITH:3
.= TRUE by XBOOLEAN:102 ;
hence  ((a 'imp' c) 'eqv' (b 'imp' c)) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  ((a 'imp' c) 'eqv' (b 'imp' c)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_7:21
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (c 'imp' a) 'eqv' (c 'imp' b)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b '<' (c 'imp' a) 'eqv' (c 'imp' b)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'eqv' b) . z = TRUE or ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE )
A1: (a 'eqv' b) . z = ((a 'imp' b) '&' (b 'imp' a)) . z by BVFUNC_4:7
.= ((a 'imp' b) . z) '&' ((b 'imp' a) . z) by MARGREL1:def_20 ;
assume A2: (a 'eqv' b) . z = TRUE ; ::_thesis: ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE
then  (a 'imp' b) . z = TRUE by A1, MARGREL1:12;
then A3: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def_8;
 (b 'imp' a) . z = TRUE by A2, A1, MARGREL1:12;
then A4: ('not' (b . z)) 'or' (a . z) = TRUE by BVFUNC_1:def_8;
A5: ((c 'imp' a) 'eqv' (c 'imp' b)) . z = (((c 'imp' a) 'imp' (c 'imp' b)) '&' ((c 'imp' b) 'imp' (c 'imp' a))) . z by BVFUNC_4:7
.= (((c 'imp' a) 'imp' (c 'imp' b)) . z) '&' (((c 'imp' b) 'imp' (c 'imp' a)) . z) by MARGREL1:def_20
.= (('not' ((c 'imp' a) . z)) 'or' ((c 'imp' b) . z)) '&' (((c 'imp' b) 'imp' (c 'imp' a)) . z) by BVFUNC_1:def_8
.= (('not' ((c 'imp' a) . z)) 'or' ((c 'imp' b) . z)) '&' (('not' ((c 'imp' b) . z)) 'or' ((c 'imp' a) . z)) by BVFUNC_1:def_8
.= (('not' (('not' (c . z)) 'or' (a . z))) 'or' ((c 'imp' b) . z)) '&' (('not' ((c 'imp' b) . z)) 'or' ((c 'imp' a) . z)) by BVFUNC_1:def_8
.= (('not' (('not' (c . z)) 'or' (a . z))) 'or' (('not' (c . z)) 'or' (b . z))) '&' (('not' ((c 'imp' b) . z)) 'or' ((c 'imp' a) . z)) by BVFUNC_1:def_8
.= (('not' (('not' (c . z)) 'or' (a . z))) 'or' (('not' (c . z)) 'or' (b . z))) '&' (('not' (('not' (c . z)) 'or' (b . z))) 'or' ((c 'imp' a) . z)) by BVFUNC_1:def_8
.= (((c . z) '&' ('not' (a . z))) 'or' (('not' (c . z)) 'or' (b . z))) '&' (((c . z) '&' ('not' (b . z))) 'or' (('not' (c . z)) 'or' (a . z))) by BVFUNC_1:def_8 ;
A6: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3;
A7: (b 'imp' a) . z = ('not' (b . z)) 'or' (a . z) by BVFUNC_1:def_8;
A8: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_(a_._z)_=_TRUE_&_((c_'imp'_a)_'eqv'_(c_'imp'_b))_._z_=_TRUE_)_or_(_b_._z_=_TRUE_&_((c_'imp'_a)_'eqv'_(c_'imp'_b))_._z_=_TRUE_)_)
percases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A3, A8, BINARITH:3;
caseA9: 'not' (a . z) = TRUE ; ::_thesis: ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE
then A10: a . z = FALSE by MARGREL1:11;
then  'not' (b . z) = TRUE by A4, BINARITH:3;
then ((c 'imp' a) 'eqv' (c 'imp' b)) . z = ((c . z) 'or' (('not' (c . z)) 'or' FALSE)) '&' ((c . z) 'or' (('not' (c . z)) 'or' FALSE)) by A5, A9, A10, MARGREL1:14
.= ((c . z) 'or' ('not' (c . z))) '&' ((c . z) 'or' ('not' (c . z))) by BINARITH:3
.= TRUE by XBOOLEAN:102 ;
hence  ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE ; ::_thesis: verum
end;
caseA11: b . z = TRUE ; ::_thesis: ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE
then  'not' (b . z) = FALSE by MARGREL1:11;
then ((c 'imp' a) 'eqv' (c 'imp' b)) . z = (FALSE 'or' (('not' (c . z)) 'or' TRUE)) '&' (FALSE 'or' (('not' (c . z)) 'or' TRUE)) by A2, A1, A7, A6, A5, A11, MARGREL1:12
.= (('not' (c . z)) 'or' TRUE) '&' (('not' (c . z)) 'or' TRUE) by BINARITH:3
.= TRUE by BINARITH:10 ;
hence  ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_7:22
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a '&' c) 'eqv' (b '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b '<' (a '&' c) 'eqv' (b '&' c)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'eqv' b) . z = TRUE or ((a '&' c) 'eqv' (b '&' c)) . z = TRUE )
A1: (a 'eqv' b) . z = ((a 'imp' b) '&' (b 'imp' a)) . z by BVFUNC_4:7
.= ((a 'imp' b) . z) '&' ((b 'imp' a) . z) by MARGREL1:def_20 ;
assume A2: (a 'eqv' b) . z = TRUE ; ::_thesis: ((a '&' c) 'eqv' (b '&' c)) . z = TRUE
then  (a 'imp' b) . z = TRUE by A1, MARGREL1:12;
then A3: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def_8;
 (b 'imp' a) . z = TRUE by A2, A1, MARGREL1:12;
then A4: ('not' (b . z)) 'or' (a . z) = TRUE by BVFUNC_1:def_8;
A5: ((a '&' c) 'eqv' (b '&' c)) . z = (((a '&' c) 'imp' (b '&' c)) '&' ((b '&' c) 'imp' (a '&' c))) . z by BVFUNC_4:7
.= (((a '&' c) 'imp' (b '&' c)) . z) '&' (((b '&' c) 'imp' (a '&' c)) . z) by MARGREL1:def_20
.= (('not' ((a '&' c) . z)) 'or' ((b '&' c) . z)) '&' (((b '&' c) 'imp' (a '&' c)) . z) by BVFUNC_1:def_8
.= (('not' ((a '&' c) . z)) 'or' ((b '&' c) . z)) '&' (('not' ((b '&' c) . z)) 'or' ((a '&' c) . z)) by BVFUNC_1:def_8
.= (('not' ((a . z) '&' (c . z))) 'or' ((b '&' c) . z)) '&' (('not' ((b '&' c) . z)) 'or' ((a '&' c) . z)) by MARGREL1:def_20
.= (('not' ((a . z) '&' (c . z))) 'or' ((b . z) '&' (c . z))) '&' (('not' ((b '&' c) . z)) 'or' ((a '&' c) . z)) by MARGREL1:def_20
.= (('not' ((a . z) '&' (c . z))) 'or' ((b . z) '&' (c . z))) '&' (('not' ((b . z) '&' (c . z))) 'or' ((a '&' c) . z)) by MARGREL1:def_20
.= ((('not' (a . z)) 'or' ('not' (c . z))) 'or' ((b . z) '&' (c . z))) '&' ((('not' (b . z)) 'or' ('not' (c . z))) 'or' ((a . z) '&' (c . z))) by MARGREL1:def_20 ;
A6: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3;
A7: (b 'imp' a) . z = ('not' (b . z)) 'or' (a . z) by BVFUNC_1:def_8;
A8: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_(a_._z)_=_TRUE_&_((a_'&'_c)_'eqv'_(b_'&'_c))_._z_=_TRUE_)_or_(_b_._z_=_TRUE_&_((a_'&'_c)_'eqv'_(b_'&'_c))_._z_=_TRUE_)_)
percases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A3, A8, BINARITH:3;
caseA9: 'not' (a . z) = TRUE ; ::_thesis: ((a '&' c) 'eqv' (b '&' c)) . z = TRUE
then A10: a . z = FALSE by MARGREL1:11;
then  'not' (b . z) = TRUE by A4, BINARITH:3;
then ((a '&' c) 'eqv' (b '&' c)) . z = ((TRUE 'or' ('not' (c . z))) 'or' FALSE) '&' ((TRUE 'or' ('not' (c . z))) 'or' FALSE) by A5, A9, A10, MARGREL1:13
.= (TRUE 'or' ('not' (c . z))) '&' (TRUE 'or' ('not' (c . z))) by BINARITH:3
.= TRUE by BINARITH:10 ;
hence  ((a '&' c) 'eqv' (b '&' c)) . z = TRUE ; ::_thesis: verum
end;
caseA11: b . z = TRUE ; ::_thesis: ((a '&' c) 'eqv' (b '&' c)) . z = TRUE
then  'not' (b . z) = FALSE by MARGREL1:11;
then ((a '&' c) 'eqv' (b '&' c)) . z = ((FALSE 'or' ('not' (c . z))) 'or' (c . z)) '&' ((FALSE 'or' ('not' (c . z))) 'or' (c . z)) by A2, A1, A7, A6, A5, A11, BINARITH:3, MARGREL1:12
.= (('not' (c . z)) 'or' (c . z)) '&' (('not' (c . z)) 'or' (c . z)) by BINARITH:3
.= TRUE by XBOOLEAN:102 ;
hence  ((a '&' c) 'eqv' (b '&' c)) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  ((a '&' c) 'eqv' (b '&' c)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_7:23
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
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'or' c) 'eqv' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b '<' (a 'or' c) 'eqv' (b 'or' c)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'eqv' b) . z = TRUE or ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE )
A1: (a 'eqv' b) . z = ((a 'imp' b) '&' (b 'imp' a)) . z by BVFUNC_4:7
.= ((a 'imp' b) . z) '&' ((b 'imp' a) . z) by MARGREL1:def_20 ;
assume A2: (a 'eqv' b) . z = TRUE ; ::_thesis: ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE
then  (a 'imp' b) . z = TRUE by A1, MARGREL1:12;
then A3: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def_8;
 (b 'imp' a) . z = TRUE by A2, A1, MARGREL1:12;
then A4: ('not' (b . z)) 'or' (a . z) = TRUE by BVFUNC_1:def_8;
A5: ((a 'or' c) 'eqv' (b 'or' c)) . z = (((a 'or' c) 'imp' (b 'or' c)) '&' ((b 'or' c) 'imp' (a 'or' c))) . z by BVFUNC_4:7
.= (((a 'or' c) 'imp' (b 'or' c)) . z) '&' (((b 'or' c) 'imp' (a 'or' c)) . z) by MARGREL1:def_20
.= (('not' ((a 'or' c) . z)) 'or' ((b 'or' c) . z)) '&' (((b 'or' c) 'imp' (a 'or' c)) . z) by BVFUNC_1:def_8
.= (('not' ((a 'or' c) . z)) 'or' ((b 'or' c) . z)) '&' (('not' ((b 'or' c) . z)) 'or' ((a 'or' c) . z)) by BVFUNC_1:def_8
.= (('not' ((a . z) 'or' (c . z))) 'or' ((b 'or' c) . z)) '&' (('not' ((b 'or' c) . z)) 'or' ((a 'or' c) . z)) by BVFUNC_1:def_4
.= (('not' ((a . z) 'or' (c . z))) 'or' ((b . z) 'or' (c . z))) '&' (('not' ((b 'or' c) . z)) 'or' ((a 'or' c) . z)) by BVFUNC_1:def_4
.= (('not' ((a . z) 'or' (c . z))) 'or' ((b . z) 'or' (c . z))) '&' (('not' ((b . z) 'or' (c . z))) 'or' ((a 'or' c) . z)) by BVFUNC_1:def_4
.= ((('not' (a . z)) '&' ('not' (c . z))) 'or' ((b . z) 'or' (c . z))) '&' ((('not' (b . z)) '&' ('not' (c . z))) 'or' ((a . z) 'or' (c . z))) by BVFUNC_1:def_4 ;
A6: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3;
A7: (b 'imp' a) . z = ('not' (b . z)) 'or' (a . z) by BVFUNC_1:def_8;
A8: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_(a_._z)_=_TRUE_&_((a_'or'_c)_'eqv'_(b_'or'_c))_._z_=_TRUE_)_or_(_b_._z_=_TRUE_&_((a_'or'_c)_'eqv'_(b_'or'_c))_._z_=_TRUE_)_)
percases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A3, A8, BINARITH:3;
caseA9: 'not' (a . z) = TRUE ; ::_thesis: ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE
then A10: a . z = FALSE by MARGREL1:11;
then  'not' (b . z) = TRUE by A4, BINARITH:3;
then ((a 'or' c) 'eqv' (b 'or' c)) . z = (('not' (c . z)) 'or' (FALSE 'or' (c . z))) '&' (('not' (c . z)) 'or' (FALSE 'or' (c . z))) by A5, A9, A10, MARGREL1:14
.= (('not' (c . z)) 'or' (c . z)) '&' (('not' (c . z)) 'or' (c . z)) by BINARITH:3
.= TRUE by XBOOLEAN:102 ;
hence  ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE ; ::_thesis: verum
end;
caseA11: b . z = TRUE ; ::_thesis: ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE
then  'not' (b . z) = FALSE by MARGREL1:11;
then ((a 'or' c) 'eqv' (b 'or' c)) . z = (FALSE 'or' (TRUE 'or' (c . z))) '&' (FALSE 'or' (TRUE 'or' (c . z))) by A2, A1, A7, A6, A5, A11, MARGREL1:12
.= (TRUE 'or' (c . z)) '&' (TRUE 'or' (c . z)) by BINARITH:3
.= TRUE by BINARITH:10 ;
hence  ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_7:24
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
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '<' ((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a
let a, b be Function of Y,BOOLEAN; ::_thesis: a '<' ((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not a . z = TRUE or (((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a) . z = TRUE )
A1: ('not' a) . z = 'not' (a . z) by MARGREL1:def_19;
assume A2: a . z = TRUE ; ::_thesis: (((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a) . z = TRUE
then A3: 'not' (a . z) = FALSE by MARGREL1:11;
A4: ((a 'eqv' b) 'eqv' (b 'eqv' a)) . z = (((a 'eqv' b) 'imp' (b 'eqv' a)) '&' ((b 'eqv' a) 'imp' (a 'eqv' b))) . z by BVFUNC_4:7
.= ((('not' (a 'eqv' b)) 'or' (b 'eqv' a)) . z) '&' ((('not' (b 'eqv' a)) 'or' (a 'eqv' b)) . z) by BVFUNC_4:8
.= ((('not' (a 'eqv' b)) . z) 'or' ((b 'eqv' a) . z)) '&' ((('not' (b 'eqv' a)) . z) 'or' ((a 'eqv' b) . z)) by BVFUNC_1:def_4
.= ((('not' ((a 'imp' b) '&' (b 'imp' a))) . z) 'or' ((b 'eqv' a) . z)) '&' ((('not' (b 'eqv' a)) . z) 'or' ((a 'eqv' b) . z)) by BVFUNC_4:7
.= ((('not' ((a 'imp' b) '&' (b 'imp' a))) . z) 'or' ((b 'eqv' a) . z)) '&' ((('not' (b 'eqv' a)) . z) 'or' (((a 'imp' b) '&' (b 'imp' a)) . z)) by BVFUNC_4:7
.= ((('not' ((a 'imp' b) '&' (b 'imp' a))) . z) 'or' (((b 'imp' a) '&' (a 'imp' b)) . z)) '&' ((('not' (b 'eqv' a)) . z) 'or' (((a 'imp' b) '&' (b 'imp' a)) . z)) by BVFUNC_4:7
.= ((('not' ((a 'imp' b) '&' (b 'imp' a))) . z) 'or' (((b 'imp' a) '&' (a 'imp' b)) . z)) '&' ((('not' ((b 'imp' a) '&' (a 'imp' b))) . z) 'or' (((a 'imp' b) '&' (b 'imp' a)) . z)) by BVFUNC_4:7
.= (('not' (((a 'imp' b) '&' (b 'imp' a)) . z)) 'or' (((b 'imp' a) '&' (a 'imp' b)) . z)) '&' (('not' (((b 'imp' a) '&' (a 'imp' b)) . z)) 'or' (((a 'imp' b) '&' (b 'imp' a)) . z)) by MARGREL1:def_19
.= (('not' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) 'or' (((b 'imp' a) '&' (a 'imp' b)) . z)) '&' (('not' (((b 'imp' a) '&' (a 'imp' b)) . z)) 'or' (((a 'imp' b) '&' (b 'imp' a)) . z)) by MARGREL1:def_20
.= (('not' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) 'or' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) '&' (('not' (((b 'imp' a) '&' (a 'imp' b)) . z)) 'or' (((a 'imp' b) '&' (b 'imp' a)) . z)) by MARGREL1:def_20
.= (('not' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) 'or' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) '&' (('not' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) 'or' (((a 'imp' b) '&' (b 'imp' a)) . z)) by MARGREL1:def_20
.= (('not' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) 'or' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) '&' (('not' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) 'or' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) by MARGREL1:def_20
.= (('not' (((('not' a) 'or' b) . z) '&' ((b 'imp' a) . z))) 'or' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) '&' (('not' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) 'or' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) by BVFUNC_4:8
.= (('not' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) 'or' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) '&' (('not' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) 'or' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) by BVFUNC_4:8
.= (('not' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) 'or' (((('not' b) 'or' a) . z) '&' ((a 'imp' b) . z))) '&' (('not' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) 'or' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) by BVFUNC_4:8
.= (('not' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) 'or' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) '&' (('not' (((b 'imp' a) . z) '&' ((a 'imp' b) . z))) 'or' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) by BVFUNC_4:8
.= (('not' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) 'or' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) '&' (('not' (((('not' b) 'or' a) . z) '&' ((a 'imp' b) . z))) 'or' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) by BVFUNC_4:8
.= (('not' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) 'or' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) '&' (('not' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) 'or' (((a 'imp' b) . z) '&' ((b 'imp' a) . z))) by BVFUNC_4:8
.= (('not' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) 'or' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) '&' (('not' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) 'or' (((('not' a) 'or' b) . z) '&' ((b 'imp' a) . z))) by BVFUNC_4:8
.= (('not' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) 'or' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) '&' (('not' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) 'or' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) by BVFUNC_4:8
.= (('not' (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' a) . z))) 'or' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) '&' (('not' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) 'or' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) by BVFUNC_1:def_4
.= (('not' (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (a . z)))) 'or' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) '&' (('not' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) 'or' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) by BVFUNC_1:def_4
.= (('not' (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (a . z)))) 'or' (((('not' b) . z) 'or' (a . z)) '&' ((('not' a) 'or' b) . z))) '&' (('not' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) 'or' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) by BVFUNC_1:def_4
.= (('not' (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (a . z)))) 'or' (((('not' b) . z) 'or' (a . z)) '&' ((('not' a) . z) 'or' (b . z)))) '&' (('not' (((('not' b) 'or' a) . z) '&' ((('not' a) 'or' b) . z))) 'or' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) by BVFUNC_1:def_4
.= (('not' (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (a . z)))) 'or' (((('not' b) . z) 'or' (a . z)) '&' ((('not' a) . z) 'or' (b . z)))) '&' (('not' (((('not' b) . z) 'or' (a . z)) '&' ((('not' a) 'or' b) . z))) 'or' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) by BVFUNC_1:def_4
.= (('not' (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (a . z)))) 'or' (((('not' b) . z) 'or' (a . z)) '&' ((('not' a) . z) 'or' (b . z)))) '&' (('not' (((('not' b) . z) 'or' (a . z)) '&' ((('not' a) . z) 'or' (b . z)))) 'or' (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' a) . z))) by BVFUNC_1:def_4
.= (('not' (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (a . z)))) 'or' (((('not' b) . z) 'or' (a . z)) '&' ((('not' a) . z) 'or' (b . z)))) '&' (('not' (((('not' b) . z) 'or' (a . z)) '&' ((('not' a) . z) 'or' (b . z)))) 'or' (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' a) . z))) by BVFUNC_1:def_4
.= (('not' ((FALSE 'or' (b . z)) '&' ((('not' b) . z) 'or' TRUE))) 'or' (((('not' b) . z) 'or' TRUE) '&' (FALSE 'or' (b . z)))) '&' (('not' (((('not' b) . z) 'or' TRUE) '&' (FALSE 'or' (b . z)))) 'or' ((FALSE 'or' (b . z)) '&' ((('not' b) . z) 'or' TRUE))) by A2, A3, A1, BVFUNC_1:def_4
.= (('not' ((b . z) '&' ((('not' b) . z) 'or' TRUE))) 'or' (((('not' b) . z) 'or' TRUE) '&' (FALSE 'or' (b . z)))) '&' (('not' (((('not' b) . z) 'or' TRUE) '&' (FALSE 'or' (b . z)))) 'or' ((FALSE 'or' (b . z)) '&' ((('not' b) . z) 'or' TRUE))) by BINARITH:3
.= (('not' ((b . z) '&' ((('not' b) . z) 'or' TRUE))) 'or' (((('not' b) . z) 'or' TRUE) '&' (b . z))) '&' (('not' (((('not' b) . z) 'or' TRUE) '&' (FALSE 'or' (b . z)))) 'or' ((FALSE 'or' (b . z)) '&' ((('not' b) . z) 'or' TRUE))) by BINARITH:3
.= (('not' ((b . z) '&' ((('not' b) . z) 'or' TRUE))) 'or' (((('not' b) . z) 'or' TRUE) '&' (b . z))) '&' (('not' (((('not' b) . z) 'or' TRUE) '&' (FALSE 'or' (b . z)))) 'or' ((b . z) '&' ((('not' b) . z) 'or' TRUE))) by BINARITH:3
.= (('not' ((b . z) '&' TRUE)) 'or' (((('not' b) . z) 'or' TRUE) '&' (b . z))) '&' (('not' (((('not' b) . z) 'or' TRUE) '&' (FALSE 'or' (b . z)))) 'or' ((b . z) '&' ((('not' b) . z) 'or' TRUE))) by BINARITH:10
.= (('not' ((b . z) '&' TRUE)) 'or' (TRUE '&' (b . z))) '&' (('not' (((('not' b) . z) 'or' TRUE) '&' (FALSE 'or' (b . z)))) 'or' ((b . z) '&' ((('not' b) . z) 'or' TRUE))) by BINARITH:10
.= (('not' ((b . z) '&' TRUE)) 'or' (TRUE '&' (b . z))) '&' (('not' (TRUE '&' (FALSE 'or' (b . z)))) 'or' ((b . z) '&' ((('not' b) . z) 'or' TRUE))) by BINARITH:10
.= (('not' ((b . z) '&' TRUE)) 'or' (TRUE '&' (b . z))) '&' (('not' (TRUE '&' (FALSE 'or' (b . z)))) 'or' ((b . z) '&' TRUE)) by BINARITH:10
.= (('not' (TRUE '&' (b . z))) 'or' (TRUE '&' (b . z))) '&' (('not' (TRUE '&' (b . z))) 'or' ((b . z) '&' TRUE)) by BINARITH:3
.= (('not' (b . z)) 'or' (TRUE '&' (b . z))) '&' (('not' (b . z)) 'or' (TRUE '&' (b . z))) by MARGREL1:14
.= (('not' (b . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (b . z)) by MARGREL1:14
.= TRUE by XBOOLEAN:102 ;
(((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a) . z = ((((a 'eqv' b) 'eqv' (b 'eqv' a)) 'imp' a) '&' (a 'imp' ((a 'eqv' b) 'eqv' (b 'eqv' a)))) . z by BVFUNC_4:7
.= ((((a 'eqv' b) 'eqv' (b 'eqv' a)) 'imp' a) . z) '&' ((a 'imp' ((a 'eqv' b) 'eqv' (b 'eqv' a))) . z) by MARGREL1:def_20
.= (('not' (((a 'eqv' b) 'eqv' (b 'eqv' a)) . z)) 'or' (a . z)) '&' ((a 'imp' ((a 'eqv' b) 'eqv' (b 'eqv' a))) . z) by BVFUNC_1:def_8
.= (('not' (((a 'eqv' b) 'eqv' (b 'eqv' a)) . z)) 'or' (a . z)) '&' (('not' (a . z)) 'or' (((a 'eqv' b) 'eqv' (b 'eqv' a)) . z)) by BVFUNC_1:def_8
.= (FALSE 'or' (a . z)) '&' (('not' (a . z)) 'or' TRUE) by A4, MARGREL1:11
.= (a . z) '&' (('not' (a . z)) 'or' TRUE) by BINARITH:3
.= TRUE '&' (a . z) by BINARITH:10
.= TRUE by A2 ;
hence  (((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_7:25
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' (a 'imp' b) 'eqv' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '<' (a 'imp' b) 'eqv' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a '<' (a 'imp' b) 'eqv' b
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not a . z = TRUE or ((a 'imp' b) 'eqv' b) . z = TRUE )
assume A1: a . z = TRUE ; ::_thesis: ((a 'imp' b) 'eqv' b) . z = TRUE
then A2: 'not' (a . z) = FALSE by MARGREL1:11;
((a 'imp' b) 'eqv' b) . z = ((('not' a) 'or' b) 'eqv' b) . z by BVFUNC_4:8
.= (((('not' a) 'or' b) 'imp' b) '&' (b 'imp' (('not' a) 'or' b))) . z by BVFUNC_4:7
.= ((('not' (('not' a) 'or' b)) 'or' b) '&' (b 'imp' (('not' a) 'or' b))) . z by BVFUNC_4:8
.= ((('not' (('not' a) 'or' b)) 'or' b) '&' (('not' b) 'or' (('not' a) 'or' b))) . z by BVFUNC_4:8
.= ((('not' (('not' a) 'or' b)) 'or' b) . z) '&' ((('not' b) 'or' (('not' a) 'or' b)) . z) by MARGREL1:def_20
.= ((('not' (('not' a) 'or' b)) . z) 'or' (b . z)) '&' ((('not' b) 'or' (('not' a) 'or' b)) . z) by BVFUNC_1:def_4
.= (('not' ((('not' a) 'or' b) . z)) 'or' (b . z)) '&' ((('not' b) 'or' (('not' a) 'or' b)) . z) by MARGREL1:def_19
.= (('not' ((('not' a) . z) 'or' (b . z))) 'or' (b . z)) '&' ((('not' b) 'or' (('not' a) 'or' b)) . z) by BVFUNC_1:def_4
.= ((('not' ('not' (a . z))) '&' ('not' (b . z))) 'or' (b . z)) '&' ((('not' b) 'or' (('not' a) 'or' b)) . z) by MARGREL1:def_19
.= (((a . z) '&' ('not' (b . z))) 'or' (b . z)) '&' ((('not' b) . z) 'or' ((('not' a) 'or' b) . z)) by BVFUNC_1:def_4
.= (((a . z) '&' ('not' (b . z))) 'or' (b . z)) '&' ((('not' b) . z) 'or' ((('not' a) . z) 'or' (b . z))) by BVFUNC_1:def_4
.= (((a . z) '&' ('not' (b . z))) 'or' (b . z)) '&' ((('not' b) . z) 'or' (('not' (a . z)) 'or' (b . z))) by MARGREL1:def_19
.= ((TRUE '&' ('not' (b . z))) 'or' (b . z)) '&' (('not' (b . z)) 'or' (FALSE 'or' (b . z))) by A1, A2, MARGREL1:def_19
.= (('not' (b . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (FALSE 'or' (b . z))) by MARGREL1:14
.= (('not' (b . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (b . z)) by BINARITH:3
.= TRUE by XBOOLEAN:102 ;
hence  ((a 'imp' b) 'eqv' b) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_7:26
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' (b 'imp' a) 'eqv' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '<' (b 'imp' a) 'eqv' a
let a, b be Function of Y,BOOLEAN; ::_thesis: a '<' (b 'imp' a) 'eqv' a
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not a . z = TRUE or ((b 'imp' a) 'eqv' a) . z = TRUE )
assume A1: a . z = TRUE ; ::_thesis: ((b 'imp' a) 'eqv' a) . z = TRUE
then A2: 'not' (a . z) = FALSE by MARGREL1:11;
((b 'imp' a) 'eqv' a) . z = ((('not' b) 'or' a) 'eqv' a) . z by BVFUNC_4:8
.= (((('not' b) 'or' a) 'imp' a) '&' (a 'imp' (('not' b) 'or' a))) . z by BVFUNC_4:7
.= ((('not' (('not' b) 'or' a)) 'or' a) '&' (a 'imp' (('not' b) 'or' a))) . z by BVFUNC_4:8
.= ((('not' (('not' b) 'or' a)) 'or' a) '&' (('not' a) 'or' (('not' b) 'or' a))) . z by BVFUNC_4:8
.= ((('not' (('not' b) 'or' a)) 'or' a) . z) '&' ((('not' a) 'or' (('not' b) 'or' a)) . z) by MARGREL1:def_20
.= ((('not' (('not' b) 'or' a)) . z) 'or' (a . z)) '&' ((('not' a) 'or' (('not' b) 'or' a)) . z) by BVFUNC_1:def_4
.= (('not' ((('not' b) 'or' a) . z)) 'or' (a . z)) '&' ((('not' a) 'or' (('not' b) 'or' a)) . z) by MARGREL1:def_19
.= (('not' ((('not' b) . z) 'or' (a . z))) 'or' (a . z)) '&' ((('not' a) 'or' (('not' b) 'or' a)) . z) by BVFUNC_1:def_4
.= ((('not' ('not' (b . z))) '&' ('not' (a . z))) 'or' (a . z)) '&' ((('not' a) 'or' (('not' b) 'or' a)) . z) by MARGREL1:def_19
.= (((b . z) '&' ('not' (a . z))) 'or' (a . z)) '&' ((('not' a) . z) 'or' ((('not' b) 'or' a) . z)) by BVFUNC_1:def_4
.= (((b . z) '&' ('not' (a . z))) 'or' (a . z)) '&' ((('not' a) . z) 'or' ((('not' b) . z) 'or' (a . z))) by BVFUNC_1:def_4
.= (((b . z) '&' ('not' (a . z))) 'or' (a . z)) '&' ((('not' a) . z) 'or' (('not' (b . z)) 'or' (a . z))) by MARGREL1:def_19
.= (((b . z) '&' ('not' (a . z))) 'or' (a . z)) '&' (('not' (a . z)) 'or' (('not' (b . z)) 'or' (a . z))) by MARGREL1:def_19
.= TRUE '&' (FALSE 'or' (('not' (b . z)) 'or' TRUE)) by A1, A2, BINARITH:10
.= FALSE 'or' (('not' (b . z)) 'or' TRUE) by MARGREL1:14
.= ('not' (b . z)) 'or' TRUE by BINARITH:3
.= TRUE by BINARITH:10 ;
hence  ((b 'imp' a) 'eqv' a) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_7:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a '&' b) 'eqv' (b '&' a)) 'eqv' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '<' ((a '&' b) 'eqv' (b '&' a)) 'eqv' a
let a, b be Function of Y,BOOLEAN; ::_thesis: a '<' ((a '&' b) 'eqv' (b '&' a)) 'eqv' a
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not a . z = TRUE or (((a '&' b) 'eqv' (b '&' a)) 'eqv' a) . z = TRUE )
assume A1: a . z = TRUE ; ::_thesis: (((a '&' b) 'eqv' (b '&' a)) 'eqv' a) . z = TRUE
A2: ((a '&' b) 'eqv' (a '&' b)) . z = (((a '&' b) 'imp' (a '&' b)) '&' ((a '&' b) 'imp' (a '&' b))) . z by BVFUNC_4:7
.= (('not' (a '&' b)) 'or' (a '&' b)) . z by BVFUNC_4:8
.= (I_el Y) . z by BVFUNC_4:6
.= TRUE by BVFUNC_1:def_11 ;
(((a '&' b) 'eqv' (b '&' a)) 'eqv' a) . z = ((((a '&' b) 'eqv' (a '&' b)) 'imp' a) '&' (a 'imp' ((a '&' b) 'eqv' (a '&' b)))) . z by BVFUNC_4:7
.= ((((a '&' b) 'eqv' (a '&' b)) 'imp' a) . z) '&' ((a 'imp' ((a '&' b) 'eqv' (a '&' b))) . z) by MARGREL1:def_20
.= ((('not' ((a '&' b) 'eqv' (a '&' b))) 'or' a) . z) '&' ((a 'imp' ((a '&' b) 'eqv' (a '&' b))) . z) by BVFUNC_4:8
.= ((('not' ((a '&' b) 'eqv' (a '&' b))) 'or' a) . z) '&' ((('not' a) 'or' ((a '&' b) 'eqv' (a '&' b))) . z) by BVFUNC_4:8
.= ((('not' ((a '&' b) 'eqv' (a '&' b))) . z) 'or' (a . z)) '&' ((('not' a) 'or' ((a '&' b) 'eqv' (a '&' b))) . z) by BVFUNC_1:def_4
.= ((('not' ((a '&' b) 'eqv' (a '&' b))) . z) 'or' (a . z)) '&' ((('not' a) . z) 'or' (((a '&' b) 'eqv' (a '&' b)) . z)) by BVFUNC_1:def_4
.= (('not' (((a '&' b) 'eqv' (a '&' b)) . z)) 'or' (a . z)) '&' ((('not' a) . z) 'or' (((a '&' b) 'eqv' (a '&' b)) . z)) by MARGREL1:def_19
.= (FALSE 'or' (a . z)) '&' ((('not' a) . z) 'or' TRUE) by A2, MARGREL1:11
.= (a . z) '&' ((('not' a) . z) 'or' TRUE) by BINARITH:3
.= TRUE '&' (a . z) by BINARITH:10
.= TRUE by A1 ;
hence  (((a '&' b) 'eqv' (b '&' a)) 'eqv' a) . z = TRUE ; ::_thesis: verum
end;