let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G)
let G be Subset of (PARTITIONS Y); for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G)
let a, u be Function of Y,BOOLEAN; for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G)
let PA be a_partition of Y; ( u is_independent_of PA,G implies u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G) )
A1:
'not' FALSE = TRUE
by MARGREL1:11;
assume A2:
u is_independent_of PA,G
; u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G)
let z be Element of Y; BVFUNC_1:def 12 ( not (u 'xor' (Ex (a,PA,G))) . z = TRUE or (Ex ((u 'xor' a),PA,G)) . z = TRUE )
A3: (u 'xor' (Ex (a,PA,G))) . z =
(u . z) 'xor' ((Ex (a,PA,G)) . z)
by BVFUNC_1:def 5
.=
(('not' (u . z)) '&' ((Ex (a,PA,G)) . z)) 'or' ((u . z) '&' ('not' ((Ex (a,PA,G)) . z)))
;
A4:
( (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE or (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = FALSE )
by XBOOLEAN:def 3;
A5:
z in EqClass (z,(CompF (PA,G)))
by EQREL_1:def 6;
assume A6:
(u 'xor' (Ex (a,PA,G))) . z = TRUE
; (Ex ((u 'xor' a),PA,G)) . z = TRUE
now ( ( ('not' (u . z)) '&' ((Ex (a,PA,G)) . z) = TRUE & (Ex ((u 'xor' a),PA,G)) . z = TRUE ) or ( (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE & (Ex ((u 'xor' a),PA,G)) . z = TRUE ) )per cases
( ('not' (u . z)) '&' ((Ex (a,PA,G)) . z) = TRUE or (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE )
by A6, A3, A4, BINARITH:3;
case A7:
('not' (u . z)) '&' ((Ex (a,PA,G)) . z) = TRUE
;
(Ex ((u 'xor' a),PA,G)) . z = TRUE then
(Ex (a,PA,G)) . z = TRUE
by MARGREL1:12;
then consider x1 being
Element of
Y such that A8:
x1 in EqClass (
z,
(CompF (PA,G)))
and A9:
a . x1 = TRUE
by BVFUNC_1:def 17;
A10:
u . z = u . x1
by A2, A5, A8, BVFUNC_1:def 15;
A11:
'not' (u . z) = TRUE
by A7, MARGREL1:12;
(u 'xor' a) . x1 =
(u . x1) 'xor' (a . x1)
by BVFUNC_1:def 5
.=
TRUE 'or' FALSE
by A11, A9, A10, MARGREL1:11
.=
TRUE
by BINARITH:10
;
hence
(Ex ((u 'xor' a),PA,G)) . z = TRUE
by A8, BVFUNC_1:def 17;
verum end; case A12:
(u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE
;
(Ex ((u 'xor' a),PA,G)) . z = TRUE then
'not' ((Ex (a,PA,G)) . z) = TRUE
by MARGREL1:12;
then
a . z <> TRUE
by A5, BVFUNC_1:def 17, MARGREL1:11;
then A13:
a . z = FALSE
by XBOOLEAN:def 3;
A14:
u . z = TRUE
by A12, MARGREL1:12;
(u 'xor' a) . z =
(u . z) 'xor' (a . z)
by BVFUNC_1:def 5
.=
FALSE 'or' TRUE
by A1, A14, A13
.=
TRUE
by BINARITH:10
;
hence
(Ex ((u 'xor' a),PA,G)) . z = TRUE
by A5, BVFUNC_1:def 17;
verum end; end; end;
hence
(Ex ((u 'xor' a),PA,G)) . z = TRUE
; verum