let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs Y,BOOLEAN holds (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c))
let a, b, c be Element of Funcs Y,BOOLEAN ; :: thesis: (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c))
let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE or ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE )
assume A1: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; :: thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE
A2: ((((('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 ;

now

assume A3: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z <> TRUE ; :: thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE
((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = ((a 'or' b) '&' ((('not' a) 'or' ('not' b)) 'or' ('not' c))) . z by BVFUNC_5:38
.= ((a 'or' b) . z) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by MARGREL1:def 21
.= ((a . z) 'or' (b . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def 7
.= ((a . z) 'or' (b . z)) '&' (((('not' a) 'or' ('not' b)) . z) 'or' (('not' c) . z)) by BVFUNC_1:def 7
.= ((a . z) 'or' (b . z)) '&' (((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by BVFUNC_1:def 7
.= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by MARGREL1:def 20
.= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' (('not' c) . z)) by MARGREL1:def 20
.= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) by MARGREL1:def 20 ;
then A4: ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) = FALSE by A3, XBOOLEAN:def 3;

now

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

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

( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def 3;
hence ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE by A1, A2, A5; :: thesis: verum

end;

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

A7: ( ('not' (a . z)) 'or' ('not' (b . z)) = TRUE or ('not' (a . z)) 'or' ('not' (b . z)) = FALSE ) by XBOOLEAN:def 3;
( 'not' (b . z) = TRUE or 'not' (b . z) = FALSE ) by XBOOLEAN:def 3;
hence ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE by A1, A2, A6, A7; :: thesis: verum

end;

end;

end;

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

end;

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