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 12 :: thesis: ( not (a 'eqv' b) . z = TRUE or ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE )
A1: (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 20 ;
assume A2: (a 'eqv' b) . z = TRUE ; :: thesis: ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE
then (a 'imp' b) . z = TRUE by A1, MARGREL1:12;
then A3: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def 8;
(b 'imp' a) . z = TRUE by A2, A1, MARGREL1:12;
then A4: ('not' (b . z)) 'or' (a . z) = TRUE by BVFUNC_1:def 8;
A5: ((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 20
.= (('not' ((c 'imp' a) . z)) 'or' ((c 'imp' b) . z)) '&' (((c 'imp' b) 'imp' (c 'imp' a)) . z) by BVFUNC_1:def 8
.= (('not' ((c 'imp' a) . z)) 'or' ((c 'imp' b) . z)) '&' (('not' ((c 'imp' b) . z)) 'or' ((c 'imp' a) . z)) by BVFUNC_1:def 8
.= (('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 8
.= (('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 8
.= (('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 8
.= (((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 8 ;
A6: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def 3;
A7: (b 'imp' a) . z = ('not' (b . z)) 'or' (a . z) by BVFUNC_1:def 8;
A8: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def 3;

now

per cases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A3, A8, BINARITH:3;

case A9: 'not' (a . z) = TRUE ; :: thesis: ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE

then A10: a . z = FALSE by MARGREL1:11;
then 'not' (b . z) = TRUE by A4, BINARITH:3;
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 A5, A9, A10, MARGREL1:14
.= ((c . z) 'or' ('not' (c . z))) '&' ((c . z) 'or' ('not' (c . z))) by BINARITH:3
.= TRUE by XBOOLEAN:102 ;
hence ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE ; :: thesis: verum

end;

case A11: b . z = TRUE ; :: thesis: ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE

then 'not' (b . z) = FALSE by MARGREL1:11;
then ((c 'imp' a) 'eqv' (c 'imp' b)) . z = (FALSE 'or' (('not' (c . z)) 'or' TRUE)) '&' (FALSE 'or' (('not' (c . z)) 'or' TRUE)) by A2, A1, A7, A6, A5, A11, MARGREL1:12
.= (('not' (c . z)) 'or' TRUE) '&' (('not' (c . z)) 'or' TRUE) by BINARITH:3
.= TRUE by BINARITH:10 ;
hence ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE ; :: thesis: verum

end;

end;

end;

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