let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs Y,BOOLEAN holds a 'eqv' b '<' (a 'eqv' c) 'eqv' (b 'eqv' c)
let a, b, c be Element of Funcs Y,BOOLEAN ; :: thesis: a 'eqv' b '<' (a 'eqv' c) 'eqv' (b 'eqv' c)
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 ,((a 'eqv' c) 'eqv' (b 'eqv' c)),z) = TRUE )
assume A1:
(a 'eqv' b) . z = TRUE
; :: thesis: K90(Y,BOOLEAN ,((a 'eqv' c) 'eqv' (b 'eqv' c)),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:
( a . z = TRUE or a . z = FALSE )
by XBOOLEAN:def 3;
then A8:
( 'not' (b . z) = TRUE or a . z = TRUE )
by A3, A6, BINARITH:7;
A9:
((a 'eqv' c) 'eqv' (b 'eqv' c)) . z = ((((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))))
now per cases
( 'not' (a . z) = TRUE or b . z = TRUE )
by A4, A5, BINARITH:7;
case A11:
b . z = TRUE
;
:: thesis: K90(Y,BOOLEAN ,((a 'eqv' c) 'eqv' (b 'eqv' c)),z) = TRUE then
'not' (b . z) = FALSE
by MARGREL1:41;
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 A1, A2, A6, A7, A9, A11, MARGREL1:45, MARGREL1:50
.=
(((('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 )))
by MARGREL1:49
.=
(((('not' c) . z) 'or' FALSE ) 'or' ((FALSE 'or' (c . z)) '&' TRUE )) '&' (((('not' c) . z) 'or' FALSE ) 'or' ((FALSE 'or' (c . z)) '&' TRUE ))
by BINARITH:19
.=
(((('not' c) . z) 'or' FALSE ) 'or' ((c . z) '&' TRUE )) '&' (((('not' c) . z) 'or' FALSE ) 'or' ((c . z) '&' TRUE ))
by BINARITH:7
.=
((('not' c) . z) 'or' (TRUE '&' (c . z))) '&' ((('not' c) . z) 'or' ((c . z) '&' TRUE ))
by BINARITH:7
.=
((('not' c) . z) 'or' (c . z)) '&' ((('not' c) . z) 'or' (c . z))
by MARGREL1:50
.=
(('not' (c . z)) 'or' (c . z)) '&' (('not' (c . z)) 'or' (c . z))
by MARGREL1:def 20
.=
TRUE
by XBOOLEAN:102
;
hence
K90(
Y,
BOOLEAN ,
((a 'eqv' c) 'eqv' (b 'eqv' c)),
z)
= TRUE
;
:: thesis: verum end;
hence
K90(Y,BOOLEAN ,((a 'eqv' c) 'eqv' (b 'eqv' c)),z) = TRUE
; :: thesis: verum