let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))
let a, b, c be Function of Y,BOOLEAN; :: thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))
A1: (((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' ((c 'or' a) '&' ('not' ((a '&' b) '&' c))) = ((((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4
.= ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4
.= (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' (('not' ((a '&' b) '&' c)) '&' ('not' ((a '&' b) '&' c))) by BVFUNC_1:4
.= (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) ;
for z being Element of Y st ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = TRUE holds
((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

proof

let z be Element of Y; :: thesis: ( ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = TRUE implies ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE )
A2: ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def 20
.= ((((a 'or' b) '&' (b 'or' c)) . z) '&' ((c 'or' a) . z)) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def 20
.= ((((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def 20
.= ((((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_5:37
.= ((((a . z) 'or' (b . z)) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def 4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def 4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def 4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' (((('not' a) 'or' ('not' b)) . z) 'or' (('not' c) . z)) by BVFUNC_1:def 4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' (((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by BVFUNC_1:def 4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' ((('not' (a . z)) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by MARGREL1:def 19
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' (('not' c) . z)) by MARGREL1:def 19
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) by MARGREL1:def 19 ;
assume A3: ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

now :: thesis: ( ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z <> TRUE implies ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE )

A4: ( ((a . z) '&' (b . z)) '&' ('not' (c . z)) = TRUE or ((a . z) '&' (b . z)) '&' ('not' (c . z)) = FALSE ) by XBOOLEAN:def 3;
assume A5: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z <> TRUE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
A6: ( ((a . z) '&' ('not' (b . z))) '&' (c . z) = TRUE or ((a . z) '&' ('not' (b . z))) '&' (c . z) = FALSE ) by XBOOLEAN:def 3;
A7: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) . z) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def 4
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def 4
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) . z) '&' (('not' c) . z)) by MARGREL1:def 20
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 20
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) . z) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 20
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 20
.= ((((('not' a) '&' b) . z) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 20
.= ((((('not' a) . z) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 20
.= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 19
.= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 19
.= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' ('not' (c . z))) by MARGREL1:def 19 ;
A8: ( ((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z)) = TRUE or ((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z)) = FALSE ) by XBOOLEAN:def 3;

now :: thesis: ( ( ('not' (a . z)) '&' (b . z) = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) or ( c . z = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) )

per cases ( ('not' (a . z)) '&' (b . z) = FALSE or c . z = FALSE ) by A5, A7, A8, A6, MARGREL1:12;

case A9: ('not' (a . z)) '&' (b . z) = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

now :: thesis: ( ( 'not' (a . z) = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) or ( b . z = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) )

per cases ( 'not' (a . z) = FALSE or b . z = FALSE ) by A9, MARGREL1:12;

case A10: 'not' (a . z) = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

now :: thesis: ( ( 'not' (b . z) = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) or ( c . z = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) )

per cases ( 'not' (b . z) = FALSE or c . z = FALSE ) by A5, A7, A6, A10, MARGREL1:12;

case 'not' (b . z) = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A7, A10; :: thesis: verum

end;

case c . z = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A7, A10; :: thesis: verum

end;

end;

end;

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; :: thesis: verum

end;

case A11: b . z = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

now :: thesis: ( ( a . z = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) or ( c . z = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) )

per cases ( a . z = FALSE or c . z = FALSE ) by A5, A7, A6, A11, MARGREL1:12;

case a . z = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A11; :: thesis: verum

end;

case c . z = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A11; :: thesis: verum

end;

end;

end;

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; :: thesis: verum

end;

end;

end;

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; :: thesis: verum

end;

case A12: c . z = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

now :: thesis: ( ( a . z = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) or ( b . z = FALSE & ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) )

per cases ( a . z = FALSE or b . z = FALSE ) by A5, A7, A4, A12, MARGREL1:12;

case a . z = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A12; :: thesis: verum

end;

case b . z = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A12; :: thesis: verum

end;

end;

end;

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; :: thesis: verum

end;

end;

end;

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; :: thesis: verum

end;

hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; :: thesis: verum

end;

then A13: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) '<' (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) ;
(((('not' c) '&' a) '&' b) 'or' ((c '&' ('not' a)) '&' b)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((c '&' a) '&' b)) by Lm4;
then (((('not' c) '&' a) '&' b) 'or' ((c '&' ('not' a)) '&' b)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then (((a '&' b) '&' ('not' c)) 'or' ((c '&' ('not' a)) '&' b)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then (((a '&' b) '&' ('not' c)) 'or' ((('not' a) '&' b) '&' c)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then (((a '&' b) '&' ('not' c)) 'or' ((('not' a) '&' b) '&' c)) 'or' ((a '&' ('not' b)) '&' c) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:8;
then A14: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((c 'or' a) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:16;
(((('not' b) '&' c) '&' a) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((b '&' c) '&' ('not' a)) '<' (b 'or' c) '&' ('not' ((b '&' c) '&' a)) by Lm4;
then (((('not' b) '&' c) '&' a) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((b '&' c) '&' ('not' a)) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then (((('not' b) '&' c) '&' a) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((('not' a) '&' b) '&' c) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then (((a '&' ('not' b)) '&' c) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((('not' a) '&' b) '&' c) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then (((a '&' ('not' b)) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((('not' a) '&' b) '&' c) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:8;
then A15: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((b 'or' c) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:16;
(((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c)) by Lm4;
then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:16;
then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' (((a 'or' b) '&' ('not' ((a '&' b) '&' c))) '&' ((b 'or' c) '&' ('not' ((a '&' b) '&' c)))) = I_el Y by A15, th18;
then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((((a 'or' b) '&' ('not' ((a '&' b) '&' c))) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:4;
then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:4;
then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' (((a 'or' b) '&' (b 'or' c)) '&' (('not' ((a '&' b) '&' c)) '&' ('not' ((a '&' b) '&' c)))) = I_el Y by BVFUNC_1:4;
then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' ((c 'or' a) '&' ('not' ((a '&' b) '&' c)))) = I_el Y by A14, th18;
then (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) by A1, BVFUNC_1:16;
hence (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) by A13, BVFUNC_1:15; :: thesis: verum