let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (c 'imp' a) 'imp' (c 'imp' b)
let a, b, c be Function of 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 :: thesis: ( ( 'not' (a . z) = TRUE & ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE ) or ( b . z = TRUE & ((c 'imp' a) 'imp' (c 'imp' b)) . z = TRUE ) )

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

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
.= (c . z) 'or' (('not' (c . z)) 'or' (b . z)) by BVFUNC_1:def 8
.= ((c . z) 'or' ('not' (c . z))) 'or' (b . z)
.= TRUE 'or' (b . z) by XBOOLEAN:102
.= TRUE ;
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
.= TRUE ;
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