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 12 :: thesis: ( not (a 'imp' b) . z = TRUE or ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE )
assume (a 'imp' b) . z = TRUE ; :: thesis: ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE
then A1: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def 8;
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:3;

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

end;

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

end;

end;

end;

hence ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE ; :: thesis: verum