let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'eqv' c) 'eqv' (b 'eqv' c)
let a, b, c be Function of Y,BOOLEAN; :: thesis: a 'eqv' b '<' (a 'eqv' c) 'eqv' (b 'eqv' c)
let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (a 'eqv' b) . z = TRUE or ((a 'eqv' c) 'eqv' (b 'eqv' 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 'eqv' c) 'eqv' (b 'eqv' 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;
A4: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def 3;
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 8;
A7: ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = (((a 'eqv' c) 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' (a 'eqv' c))) . z by BVFUNC_4:7
.= ((((a 'imp' c) '&' (c 'imp' a)) 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' (a 'eqv' c))) . z by BVFUNC_4:7
.= ((((a 'imp' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' ((b 'eqv' c) 'imp' (a 'eqv' c))) . z by BVFUNC_4:7
.= ((((a 'imp' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' (a 'eqv' c))) . z by BVFUNC_4:7
.= ((((a 'imp' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:7
.= ((((('not' a) 'or' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' ((('not' a) 'or' c) '&' (c 'imp' a)))) . z by BVFUNC_4:8
.= ((((('not' a) 'or' c) '&' (('not' c) 'or' a)) 'imp' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_4:8
.= ((('not' ((('not' a) 'or' c) '&' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_4:8
.= ((('not' ((('not' a) 'or' c) '&' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (('not' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_4:8
.= (((('not' (('not' a) 'or' c)) 'or' ('not' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (('not' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:14
.= (((('not' (('not' a) 'or' c)) 'or' ('not' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' ((('not' (('not' b) 'or' c)) 'or' ('not' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:14
.= ((((('not' ('not' a)) '&' ('not' c)) 'or' ('not' (('not' c) 'or' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' ((('not' (('not' b) 'or' c)) 'or' ('not' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:13
.= ((((('not' ('not' a)) '&' ('not' c)) 'or' (('not' ('not' c)) '&' ('not' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' ((('not' (('not' b) 'or' c)) 'or' ('not' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:13
.= ((((('not' ('not' a)) '&' ('not' c)) 'or' (('not' ('not' c)) '&' ('not' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' ('not' b)) '&' ('not' c)) 'or' ('not' (('not' c) 'or' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:13
.= ((((a '&' ('not' c)) 'or' (c '&' ('not' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b '&' ('not' c)) 'or' (('not' ('not' c)) '&' ('not' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a)))) . z by BVFUNC_1:13
.= ((((a '&' ('not' c)) 'or' (c '&' ('not' a))) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) . z) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a))) . z) by MARGREL1:def 20
.= ((((a '&' ('not' c)) 'or' (c '&' ('not' a))) . z) 'or' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) . z)) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) 'or' ((('not' a) 'or' c) '&' (('not' c) 'or' a))) . z) by BVFUNC_1:def 4
.= ((((a '&' ('not' c)) 'or' (c '&' ('not' a))) . z) 'or' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) . z)) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) . z) 'or' (((('not' a) 'or' c) '&' (('not' c) 'or' a)) . z)) by BVFUNC_1:def 4
.= ((((a '&' ('not' c)) . z) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) . z)) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) . z) 'or' (((('not' a) 'or' c) '&' (('not' c) 'or' a)) . z)) by BVFUNC_1:def 4
.= ((((a '&' ('not' c)) . z) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) 'or' (c '&' ('not' b))) . z) 'or' (((('not' a) 'or' c) '&' (('not' c) 'or' a)) . z)) by MARGREL1:def 20
.= ((((a '&' ('not' c)) . z) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) '&' (('not' c) 'or' a)) . z)) by BVFUNC_1:def 4
.= ((((a '&' ('not' c)) . z) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def 20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c '&' ('not' a)) . z)) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def 20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) 'or' c) . z) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def 20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) 'or' b) . z))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by BVFUNC_1:def 4
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b '&' ('not' c)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by BVFUNC_1:def 4
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c '&' ('not' b)) . z)) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def 20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) 'or' c) . z) '&' ((('not' c) 'or' a) . z))) by MARGREL1:def 20
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) 'or' a) . z))) by BVFUNC_1:def 4
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' a) . z))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by BVFUNC_1:def 4
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (a . z)))) 'or' (((('not' b) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by MARGREL1:def 19
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (a . z)))) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by MARGREL1:def 19
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (a . z)))) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (((('not' a) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by MARGREL1:def 19
.= ((((a . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (a . z)))) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((('not' (a . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (a . z)))) by MARGREL1:def 19 ;
(b 'imp' a) . z = TRUE by A2, A1, MARGREL1:12;
then A8: ( 'not' (b . z) = TRUE or a . z = TRUE ) by A6, A4;

now :: thesis: ( ( 'not' (a . z) = TRUE & ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE ) or ( b . z = TRUE & ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE ) )

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

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

then a . z = FALSE ;
then ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = ((FALSE 'or' ((c . z) '&' TRUE)) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((TRUE 'or' (c . z)) '&' ((('not' c) . z) 'or' FALSE))) by A7
.= ((FALSE 'or' (c . z)) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((TRUE 'or' (c . z)) '&' ((('not' c) . z) 'or' FALSE)))
.= ((c . z) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((TRUE 'or' (c . z)) '&' ((('not' c) . z) 'or' FALSE)))
.= ((c . z) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' ((TRUE 'or' (c . z)) '&' (('not' c) . z)))
.= ((c . z) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (TRUE '&' (('not' c) . z)))
.= ((c . z) 'or' ((('not' (b . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z))
.= (((c . z) 'or' ((c . z) 'or' ('not' (b . z)))) '&' ((c . z) 'or' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by XBOOLEAN:9
.= ((((c . z) 'or' (c . z)) 'or' ('not' (b . z))) '&' ((c . z) 'or' ((('not' c) . z) 'or' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z))
.= (((c . z) 'or' ('not' (b . z))) '&' (((c . z) 'or' (('not' c) . z)) 'or' (b . z))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z))
.= (((c . z) 'or' ('not' (b . z))) '&' (((c . z) 'or' ('not' (c . z))) 'or' (b . z))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by MARGREL1:def 19
.= (((c . z) 'or' ('not' (b . z))) '&' (TRUE 'or' (b . z))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z)) by XBOOLEAN:102
.= (TRUE '&' ((c . z) 'or' ('not' (b . z)))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z))
.= ((c . z) 'or' ('not' (b . z))) '&' ((((b . z) '&' (('not' c) . z)) 'or' ((c . z) '&' ('not' (b . z)))) 'or' (('not' c) . z))
.= ((c . z) 'or' ('not' (b . z))) '&' (((b . z) '&' (('not' c) . z)) 'or' ((('not' c) . z) 'or' ((c . z) '&' ('not' (b . z)))))
.= ((c . z) 'or' ('not' (b . z))) '&' (((b . z) '&' (('not' c) . z)) 'or' (((('not' c) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' ('not' (b . z))))) by XBOOLEAN:9
.= ((c . z) 'or' ('not' (b . z))) '&' (((b . z) '&' (('not' c) . z)) 'or' ((('not' (c . z)) 'or' (c . z)) '&' ((('not' c) . z) 'or' ('not' (b . z))))) by MARGREL1:def 19
.= ((c . z) 'or' ('not' (b . z))) '&' (((b . z) '&' (('not' c) . z)) 'or' (TRUE '&' ((('not' c) . z) 'or' ('not' (b . z))))) by XBOOLEAN:102
.= ((c . z) 'or' ('not' (b . z))) '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' ((b . z) '&' (('not' c) . z)))
.= ((c . z) 'or' ('not' (b . z))) '&' ((((('not' c) . z) 'or' ('not' (b . z))) 'or' (b . z)) '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' (('not' c) . z))) by XBOOLEAN:9
.= ((c . z) 'or' ('not' (b . z))) '&' (((('not' c) . z) 'or' (('not' (b . z)) 'or' (b . z))) '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' (('not' c) . z)))
.= ((c . z) 'or' ('not' (b . z))) '&' (((('not' c) . z) 'or' TRUE) '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' (('not' c) . z))) by XBOOLEAN:102
.= ((c . z) 'or' ('not' (b . z))) '&' (TRUE '&' (((('not' c) . z) 'or' ('not' (b . z))) 'or' (('not' c) . z)))
.= ((c . z) 'or' ('not' (b . z))) '&' ((('not' (b . z)) 'or' (('not' c) . z)) 'or' (('not' c) . z))
.= ((c . z) 'or' ('not' (b . z))) '&' (('not' (b . z)) 'or' ((('not' c) . z) 'or' (('not' c) . z)))
.= (('not' (b . z)) '&' ((c . z) 'or' ('not' (b . z)))) 'or' (((c . z) 'or' ('not' (b . z))) '&' (('not' c) . z)) by XBOOLEAN:8
.= ((('not' (b . z)) '&' (c . z)) 'or' (('not' (b . z)) '&' ('not' (b . z)))) 'or' ((('not' c) . z) '&' ((c . z) 'or' ('not' (b . z)))) by XBOOLEAN:8
.= ((('not' (b . z)) '&' (c . z)) 'or' ('not' (b . z))) 'or' (((('not' c) . z) '&' (c . z)) 'or' ((('not' c) . z) '&' ('not' (b . z)))) by XBOOLEAN:8
.= ((('not' (b . z)) '&' (c . z)) 'or' ('not' (b . z))) 'or' (((c . z) '&' ('not' (c . z))) 'or' ((('not' c) . z) '&' ('not' (b . z)))) by MARGREL1:def 19
.= ((('not' (b . z)) '&' (c . z)) 'or' ('not' (b . z))) 'or' (FALSE 'or' ((('not' c) . z) '&' ('not' (b . z)))) by XBOOLEAN:138
.= (('not' (b . z)) 'or' (('not' (b . z)) '&' (c . z))) 'or' ((('not' c) . z) '&' ('not' (b . z)))
.= ('not' (b . z)) 'or' ((('not' (b . z)) '&' (c . z)) 'or' ((('not' c) . z) '&' ('not' (b . z))))
.= TRUE by A8, A9 ;
hence ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE ; :: thesis: verum

end;

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

then 'not' (b . z) = FALSE ;
then ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = (((('not' c) . z) 'or' (FALSE '&' (c . z))) 'or' ((FALSE 'or' (c . z)) '&' ((('not' c) . z) 'or' TRUE))) '&' (((('not' c) . z) 'or' ((c . z) '&' FALSE)) 'or' ((FALSE 'or' (c . z)) '&' ((('not' c) . z) 'or' TRUE))) by A2, A1, A6, A4, A7
.= (((('not' c) . z) 'or' FALSE) 'or' ((FALSE 'or' (c . z)) '&' ((('not' c) . z) 'or' TRUE))) '&' (((('not' c) . z) 'or' FALSE) 'or' ((FALSE 'or' (c . z)) '&' ((('not' c) . z) 'or' TRUE)))
.= (((('not' c) . z) 'or' FALSE) 'or' ((FALSE 'or' (c . z)) '&' TRUE)) '&' (((('not' c) . z) 'or' FALSE) 'or' ((FALSE 'or' (c . z)) '&' TRUE))
.= (((('not' c) . z) 'or' FALSE) 'or' ((c . z) '&' TRUE)) '&' (((('not' c) . z) 'or' FALSE) 'or' ((c . z) '&' TRUE))
.= ((('not' c) . z) 'or' (TRUE '&' (c . z))) '&' ((('not' c) . z) 'or' ((c . z) '&' TRUE))
.= ((('not' c) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (c . z))
.= (('not' (c . z)) 'or' (c . z)) '&' (('not' (c . z)) 'or' (c . z)) by MARGREL1:def 19
.= TRUE by XBOOLEAN:102 ;
hence ((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = TRUE ; :: thesis: verum

end;

end;

end;

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