let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs Y,BOOLEAN holds a 'eqv' b '<' (c 'imp' a) 'eqv' (c 'imp' b)
let a, b, c be Element of Funcs Y,BOOLEAN ; :: thesis: a 'eqv' b '<' (c 'imp' a) 'eqv' (c 'imp' b)
let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not K90(Y,BOOLEAN ,(a 'eqv' b),z) = TRUE or K90(Y,BOOLEAN ,((c 'imp' a) 'eqv' (c 'imp' b)),z) = TRUE )
assume A1: (a 'eqv' b) . z = TRUE ; :: thesis: K90(Y,BOOLEAN ,((c 'imp' a) 'eqv' (c 'imp' b)),z) = TRUE
A2: (a 'eqv' b) . z = ((a 'imp' b) '&' (b 'imp' a)) . z by BVFUNC_4:7
.= ((a 'imp' b) . z) '&' ((b 'imp' a) . z) by MARGREL1:def 21 ;
then A3: ( (a 'imp' b) . z = TRUE & (b 'imp' a) . z = TRUE ) by A1, MARGREL1:45;
then A4: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def 11;
A5: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def 3;
A6: (b 'imp' a) . z = ('not' (b . z)) 'or' (a . z) by BVFUNC_1:def 11;
A7: ('not' (b . z)) 'or' (a . z) = TRUE by A3, BVFUNC_1:def 11;
A8: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def 3;
A9: ((c 'imp' a) 'eqv' (c 'imp' b)) . z = (((c 'imp' a) 'imp' (c 'imp' b)) '&' ((c 'imp' b) 'imp' (c 'imp' a))) . z by BVFUNC_4:7
.= (((c 'imp' a) 'imp' (c 'imp' b)) . z) '&' (((c 'imp' b) 'imp' (c 'imp' a)) . z) by MARGREL1:def 21
.= (('not' ((c 'imp' a) . z)) 'or' ((c 'imp' b) . z)) '&' (((c 'imp' b) 'imp' (c 'imp' a)) . z) by BVFUNC_1:def 11
.= (('not' ((c 'imp' a) . z)) 'or' ((c 'imp' b) . z)) '&' (('not' ((c 'imp' b) . z)) 'or' ((c 'imp' a) . z)) by BVFUNC_1:def 11
.= (('not' (('not' (c . z)) 'or' (a . z))) 'or' ((c 'imp' b) . z)) '&' (('not' ((c 'imp' b) . z)) 'or' ((c 'imp' a) . z)) by BVFUNC_1:def 11
.= (('not' (('not' (c . z)) 'or' (a . z))) 'or' (('not' (c . z)) 'or' (b . z))) '&' (('not' ((c 'imp' b) . z)) 'or' ((c 'imp' a) . z)) by BVFUNC_1:def 11
.= (('not' (('not' (c . z)) 'or' (a . z))) 'or' (('not' (c . z)) 'or' (b . z))) '&' (('not' (('not' (c . z)) 'or' (b . z))) 'or' ((c 'imp' a) . z)) by BVFUNC_1:def 11
.= (((c . z) '&' ('not' (a . z))) 'or' (('not' (c . z)) 'or' (b . z))) '&' (((c . z) '&' ('not' (b . z))) 'or' (('not' (c . z)) 'or' (a . z))) by BVFUNC_1:def 11 ;

now

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

case A10: 'not' (a . z) = TRUE ; :: thesis: K90(Y,BOOLEAN ,((c 'imp' a) 'eqv' (c 'imp' b)),z) = TRUE

then A11: a . z = FALSE by MARGREL1:41;
then 'not' (b . z) = TRUE by A7, BINARITH:7;
then ((c 'imp' a) 'eqv' (c 'imp' b)) . z = ((c . z) 'or' (('not' (c . z)) 'or' FALSE )) '&' ((c . z) 'or' (('not' (c . z)) 'or' FALSE )) by A9, A10, A11, MARGREL1:50
.= ((c . z) 'or' ('not' (c . z))) '&' ((c . z) 'or' ('not' (c . z))) by BINARITH:7
.= TRUE by XBOOLEAN:102 ;
hence K90(Y,BOOLEAN ,((c 'imp' a) 'eqv' (c 'imp' b)),z) = TRUE ; :: thesis: verum

end;

case A12: b . z = TRUE ; :: thesis: K90(Y,BOOLEAN ,((c 'imp' a) 'eqv' (c 'imp' b)),z) = TRUE

then 'not' (b . z) = FALSE by MARGREL1:41;
then ((c 'imp' a) 'eqv' (c 'imp' b)) . z = (FALSE 'or' (('not' (c . z)) 'or' TRUE )) '&' (FALSE 'or' (('not' (c . z)) 'or' TRUE )) by A1, A2, A6, A8, A9, A12, MARGREL1:45
.= (('not' (c . z)) 'or' TRUE ) '&' (('not' (c . z)) 'or' TRUE ) by BINARITH:7
.= TRUE by BINARITH:19 ;
hence K90(Y,BOOLEAN ,((c 'imp' a) 'eqv' (c 'imp' b)),z) = TRUE ; :: thesis: verum

end;

end;

end;

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