let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds a 'xor' b '<' ('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))
let G be Subset of (PARTITIONS Y); :: thesis: for a, b being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds a 'xor' b '<' ('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))
let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: for PA being a_partition of Y holds a 'xor' b '<' ('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))
let PA be a_partition of Y; :: thesis: a 'xor' b '<' ('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))
A1:
Ex ('not' a),PA,G = B_SUP ('not' a),(CompF PA,G)
by BVFUNC_2:def 10;
A2:
Ex ('not' b),PA,G = B_SUP ('not' b),(CompF PA,G)
by BVFUNC_2:def 10;
let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not (a 'xor' b) . z = TRUE or (('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))) . z = TRUE )
assume A3:
(a 'xor' b) . z = TRUE
; :: thesis: (('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))) . z = TRUE
A4: (a 'xor' b) . z =
(a . z) 'xor' (b . z)
by BVFUNC_1:def 8
.=
(('not' (a . z)) '&' (b . z)) 'or' ((a . z) '&' ('not' (b . z)))
;
A5:
( (a . z) '&' ('not' (b . z)) = TRUE or (a . z) '&' ('not' (b . z)) = FALSE )
by XBOOLEAN:def 3;
A6:
( z in EqClass z,(CompF PA,G) & EqClass z,(CompF PA,G) in CompF PA,G )
by EQREL_1:def 8;
A7:
FALSE '&' TRUE = FALSE
by MARGREL1:49;
per cases
( ('not' (a . z)) '&' (b . z) = TRUE or (a . z) '&' ('not' (b . z)) = TRUE )
by A3, A4, A5, BINARITH:7;
suppose
('not' (a . z)) '&' (b . z) = TRUE
;
:: thesis: (('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))) . z = TRUE then A8:
(
'not' (a . z) = TRUE &
b . z = TRUE )
by MARGREL1:45;
then
('not' a) . z = TRUE
by MARGREL1:def 20;
then A9:
(B_SUP ('not' a),(CompF PA,G)) . z = TRUE
by A6, BVFUNC_1:def 20;
(B_SUP b,(CompF PA,G)) . z = TRUE
by A6, A8, BVFUNC_1:def 20;
then A10:
(Ex b,PA,G) . z = TRUE
by BVFUNC_2:def 10;
A11:
((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G)) . z =
((Ex ('not' a),PA,G) . z) 'xor' ((Ex b,PA,G) . z)
by BVFUNC_1:def 8
.=
FALSE
by A1, A7, A9, A10, MARGREL1:41
;
A12:
('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G))) . z = 'not' (((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)) . z)
by MARGREL1:def 20;
thus (('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))) . z =
(('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) . z) 'or' (('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G))) . z)
by BVFUNC_1:def 7
.=
('not' FALSE ) 'or' ('not' (((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)) . z))
by A11, A12, MARGREL1:def 20
.=
TRUE 'or' ('not' (((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)) . z))
by MARGREL1:41
.=
TRUE
by BINARITH:19
;
:: thesis: verum end; suppose
(a . z) '&' ('not' (b . z)) = TRUE
;
:: thesis: (('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))) . z = TRUE then A13:
(
a . z = TRUE &
'not' (b . z) = TRUE )
by MARGREL1:45;
then
('not' b) . z = TRUE
by MARGREL1:def 20;
then A14:
(B_SUP ('not' b),(CompF PA,G)) . z = TRUE
by A6, BVFUNC_1:def 20;
(B_SUP a,(CompF PA,G)) . z = TRUE
by A6, A13, BVFUNC_1:def 20;
then A15:
(Ex a,PA,G) . z = TRUE
by BVFUNC_2:def 10;
A16:
((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)) . z =
((Ex a,PA,G) . z) 'xor' ((Ex ('not' b),PA,G) . z)
by BVFUNC_1:def 8
.=
FALSE
by A2, A7, A14, A15, MARGREL1:41
;
A17:
('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G))) . z = 'not' (((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)) . z)
by MARGREL1:def 20;
thus (('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))) . z =
(('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) . z) 'or' (('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G))) . z)
by BVFUNC_1:def 7
.=
('not' (((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G)) . z)) 'or' ('not' FALSE )
by A16, A17, MARGREL1:def 20
.=
('not' (((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G)) . z)) 'or' TRUE
by MARGREL1:41
.=
TRUE
by BINARITH:19
;
:: thesis: verum end;