let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs Y,BOOLEAN holds a 'imp' b '<' (c 'imp' a) 'imp' (c 'imp' b)
let a, b, c be Element of Funcs Y,BOOLEAN ; :: thesis: a 'imp' b '<' (c 'imp' a) 'imp' (c 'imp' b)
let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not K90(Y,BOOLEAN ,(a 'imp' b),z) = TRUE or K90(Y,BOOLEAN ,((c 'imp' a) 'imp' (c 'imp' b)),z) = TRUE )
assume (a 'imp' b) . z = TRUE ; :: thesis: K90(Y,BOOLEAN ,((c 'imp' a) 'imp' (c 'imp' b)),z) = TRUE
then A1: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def 11;
A2: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def 3;

now

per cases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A1, A2, BINARITH:7;

case A3: 'not' (a . z) = TRUE ; :: thesis: K90(Y,BOOLEAN ,((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 11
.= ('not' (('not' (c . z)) 'or' (a . z))) 'or' ((c 'imp' b) . z) by BVFUNC_1:def 11
.= (c . z) 'or' ((c 'imp' b) . z) by A3, MARGREL1:50
.= (c . z) 'or' (('not' (c . z)) 'or' (b . z)) by BVFUNC_1:def 11
.= ((c . z) 'or' ('not' (c . z))) 'or' (b . z) by BINARITH:20
.= TRUE 'or' (b . z) by XBOOLEAN:102
.= TRUE by BINARITH:19 ;
hence K90(Y,BOOLEAN ,((c 'imp' a) 'imp' (c 'imp' b)),z) = TRUE ; :: thesis: verum

end;

case A4: b . z = TRUE ; :: thesis: K90(Y,BOOLEAN ,((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 11
.= ('not' (('not' (c . z)) 'or' (a . z))) 'or' ((c 'imp' b) . z) by BVFUNC_1:def 11
.= ('not' (('not' (c . z)) 'or' (a . z))) 'or' (('not' (c . z)) 'or' TRUE ) by A4, BVFUNC_1:def 11
.= ('not' (('not' (c . z)) 'or' (a . z))) 'or' TRUE by BINARITH:19
.= TRUE by BINARITH:19 ;
hence K90(Y,BOOLEAN ,((c 'imp' a) 'imp' (c 'imp' b)),z) = TRUE ; :: thesis: verum

end;

end;

end;

hence K90(Y,BOOLEAN ,((c 'imp' a) 'imp' (c 'imp' b)),z) = TRUE ; :: thesis: verum