let Y be non empty set ; :: thesis: for a, b, c being Function of 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 Function of 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 12 :: 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 )
A1: ((((('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 ;
assume A2: ((((('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

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

A3: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = ((a 'or' b) '&' ((('not' a) 'or' ('not' b)) 'or' ('not' c))) . z by BVFUNC_5:37
.= ((a 'or' b) . z) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by MARGREL1:def 20
.= ((a . z) 'or' (b . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def 4
.= ((a . z) 'or' (b . z)) '&' (((('not' a) 'or' ('not' b)) . z) 'or' (('not' c) . z)) by BVFUNC_1:def 4
.= ((a . z) 'or' (b . z)) '&' (((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by BVFUNC_1:def 4
.= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by MARGREL1:def 19
.= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' (('not' c) . z)) by MARGREL1:def 19
.= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) by MARGREL1:def 19 ;
assume ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z <> TRUE ; :: thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE
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 :: thesis: ( ( (a . z) 'or' (b . z) = FALSE & ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ) or ( (('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z)) = FALSE & ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ) )

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

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 A2, A1, 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' (b . z) = TRUE or 'not' (b . z) = FALSE ) by XBOOLEAN:def 3;
( ('not' (a . z)) 'or' ('not' (b . z)) = TRUE or ('not' (a . z)) 'or' ('not' (b . z)) = FALSE ) by XBOOLEAN:def 3;
hence ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE by A2, A1, 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