let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'or' c) 'eqv' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; :: thesis: a 'eqv' b '<' (a 'or' c) 'eqv' (b 'or' c)
let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (a 'eqv' b) . z = TRUE or ((a 'or' c) 'eqv' (b 'or' c)) . 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: ((a 'or' c) 'eqv' (b 'or' c)) . 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: ((a 'or' c) 'eqv' (b 'or' c)) . z = (((a 'or' c) 'imp' (b 'or' c)) '&' ((b 'or' c) 'imp' (a 'or' c))) . z by BVFUNC_4:7
.= (((a 'or' c) 'imp' (b 'or' c)) . z) '&' (((b 'or' c) 'imp' (a 'or' c)) . z) by MARGREL1:def 20
.= (('not' ((a 'or' c) . z)) 'or' ((b 'or' c) . z)) '&' (((b 'or' c) 'imp' (a 'or' c)) . z) by BVFUNC_1:def 8
.= (('not' ((a 'or' c) . z)) 'or' ((b 'or' c) . z)) '&' (('not' ((b 'or' c) . z)) 'or' ((a 'or' c) . z)) by BVFUNC_1:def 8
.= (('not' ((a . z) 'or' (c . z))) 'or' ((b 'or' c) . z)) '&' (('not' ((b 'or' c) . z)) 'or' ((a 'or' c) . z)) by BVFUNC_1:def 4
.= (('not' ((a . z) 'or' (c . z))) 'or' ((b . z) 'or' (c . z))) '&' (('not' ((b 'or' c) . z)) 'or' ((a 'or' c) . z)) by BVFUNC_1:def 4
.= (('not' ((a . z) 'or' (c . z))) 'or' ((b . z) 'or' (c . z))) '&' (('not' ((b . z) 'or' (c . z))) 'or' ((a 'or' c) . z)) by BVFUNC_1:def 4
.= ((('not' (a . z)) '&' ('not' (c . z))) 'or' ((b . z) 'or' (c . z))) '&' ((('not' (b . z)) '&' ('not' (c . z))) 'or' ((a . z) 'or' (c . z))) by BVFUNC_1:def 4 ;
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 :: thesis: ( ( 'not' (a . z) = TRUE & ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE ) or ( b . z = TRUE & ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE ) )

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

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

then a . z = FALSE ;
then 'not' (b . z) = TRUE by A4;
then ((a 'or' c) 'eqv' (b 'or' c)) . z = (('not' (c . z)) 'or' (FALSE 'or' (c . z))) '&' (('not' (c . z)) 'or' (FALSE 'or' (c . z))) by A5, A9
.= (('not' (c . z)) 'or' (c . z)) '&' (('not' (c . z)) 'or' (c . z))
.= TRUE by XBOOLEAN:102 ;
hence ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE ; :: thesis: verum

end;

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

then 'not' (b . z) = FALSE ;
then ((a 'or' c) 'eqv' (b 'or' c)) . z = (FALSE 'or' (TRUE 'or' (c . z))) '&' (FALSE 'or' (TRUE 'or' (c . z))) by A2, A1, A7, A6, A5
.= (TRUE 'or' (c . z)) '&' (TRUE 'or' (c . z))
.= TRUE ;
hence ((a 'or' c) 'eqv' (b 'or' c)) . z = TRUE ; :: thesis: verum

end;

end;

end;

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