let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs 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 Element of Funcs 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))
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 )
assume A1: ((((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
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 21
.= ((((a 'or' b) '&' (b 'or' c)) . z) '&' ((c 'or' a) . z)) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def 21
.= ((((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def 21
.= ((((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_5:38
.= ((((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 7
.= ((((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 7
.= ((((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 7
.= ((((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 7
.= ((((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 7
.= ((((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 20
.= ((((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 20
.= ((((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 20 ;

now

assume A3: ((((('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
A4: ((((('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 7
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def 7
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) . z) '&' (('not' c) . z)) by MARGREL1:def 21
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 21
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) . z) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 21
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def 21
.= ((((('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 21
.= ((((('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 21
.= (((('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 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 ;
A5: ( ((('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;
A6: ( ((a . z) '&' (b . z)) '&' ('not' (c . z)) = TRUE or ((a . z) '&' (b . z)) '&' ('not' (c . z)) = FALSE ) by XBOOLEAN:def 3;
A7: ( ((a . z) '&' ('not' (b . z))) '&' (c . z) = TRUE or ((a . z) '&' ('not' (b . z))) '&' (c . z) = FALSE ) by XBOOLEAN:def 3;

now

per cases ( ('not' (a . z)) '&' (b . z) = FALSE or c . z = FALSE ) by A3, A4, A5, A7, MARGREL1:45;

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

now

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

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

now

per cases ( 'not' (b . z) = FALSE or c . z = FALSE ) by A3, A4, A7, A9, MARGREL1:45;

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 A1, A2, A4, A9; :: 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 A1, A2, A4, A9; :: 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 A10: b . z = FALSE ; :: thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE

now

per cases ( a . z = FALSE or c . z = FALSE ) by A3, A4, A7, A10, MARGREL1:45;

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 A1, A2, 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 A1, A2, 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;

end;

end;

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

end;

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

now

per cases ( a . z = FALSE or b . z = FALSE ) by A3, A4, A6, A11, MARGREL1:45;

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 A1, A2, A11; :: 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 A1, 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;

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

end;

then A12: (((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 BVFUNC_1:def 15;
A13: (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c)) by Lm4;
(((('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:7;
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:7;
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:7;
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:7;
then A14: (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:11;
(((('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:7;
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:7;
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:7;
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:7;
then A15: (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:11;
A16: ((((('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 A13, BVFUNC_1:19;
A17: ((((('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 A14, BVFUNC_1:19;
A18: ((((('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 A15, BVFUNC_1:19;
((((('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 A16, A17, BVFUNC_6:18;
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:7;
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:7;
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:7;
then A19: ((((('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 A18, BVFUNC_6:18;
(((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:7
.= ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:7
.= (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' (('not' ((a '&' b) '&' c)) '&' ('not' ((a '&' b) '&' c))) by BVFUNC_1:7
.= (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) ;
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 A19, BVFUNC_1:19;
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 A12, BVFUNC_1:18; :: thesis: verum