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

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

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

then a . z = FALSE ;
then 'not' (b . z) = TRUE by A4;
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
.= ((c . z) 'or' ('not' (c . z))) '&' ((c . z) 'or' ('not' (c . z)))
.= TRUE by XBOOLEAN:102 ;
hence ((c 'imp' a) 'eqv' (c 'imp' b)) . z = TRUE ; :: thesis: verum

end;

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

then 'not' (b . z) = FALSE ;
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, A5, MARGREL1:12
.= (('not' (c . z)) 'or' TRUE) '&' (('not' (c . z)) 'or' TRUE)
.= TRUE ;
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