let Y be non empty set ; 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); 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 ; 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; 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;
let z be Element of Y; BVFUNC_1:def 15 ( 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 )
A2:
Ex ('not' b),PA,G = B_SUP ('not' b),(CompF PA,G)
by BVFUNC_2:def 10;
A3:
( (a . z) '&' ('not' (b . z)) = TRUE or (a . z) '&' ('not' (b . z)) = FALSE )
by XBOOLEAN:def 3;
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:
z in EqClass z,(CompF PA,G)
by EQREL_1:def 8;
A6:
FALSE '&' TRUE = FALSE
by MARGREL1:49;
assume A7:
(a 'xor' b) . z = TRUE
; (('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
per cases
( ('not' (a . z)) '&' (b . z) = TRUE or (a . z) '&' ('not' (b . z)) = TRUE )
by A7, A4, A3, BINARITH:7;
suppose A8:
('not' (a . z)) '&' (b . z) = TRUE
;
(('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
'not' (a . 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 A5, BVFUNC_1:def 20;
A10:
('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;
b . z = TRUE
by A8, MARGREL1:45;
then
(B_SUP b,(CompF PA,G)) . z = TRUE
by A5, BVFUNC_1:def 20;
then A11:
(Ex b,PA,G) . z = TRUE
by BVFUNC_2:def 10;
A12:
((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, A6, A9, A11, MARGREL1:41
;
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 A12, A10, MARGREL1:def 20
.=
TRUE 'or' ('not' (((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)) . z))
by MARGREL1:41
.=
TRUE
by BINARITH:19
;
verum end; suppose A13:
(a . z) '&' ('not' (b . z)) = TRUE
;
(('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
a . z = TRUE
by MARGREL1:45;
then
(B_SUP a,(CompF PA,G)) . z = TRUE
by A5, BVFUNC_1:def 20;
then A14:
(Ex a,PA,G) . z = TRUE
by BVFUNC_2:def 10;
A15:
('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;
'not' (b . z) = TRUE
by A13, MARGREL1:45;
then
('not' b) . z = TRUE
by MARGREL1:def 20;
then A16:
(B_SUP ('not' b),(CompF PA,G)) . z = TRUE
by A5, BVFUNC_1:def 20;
A17:
((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, A6, A16, A14, MARGREL1:41
;
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 A17, A15, MARGREL1:def 20
.=
('not' (((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G)) . z)) 'or' TRUE
by MARGREL1:41
.=
TRUE
by BINARITH:19
;
verum end;