let Y be non empty set ; :: thesis: 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
All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G))
let G be Subset of (PARTITIONS Y); :: thesis: for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G))
let a, u be Function of Y,BOOLEAN; :: thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G))
let PA be a_partition of Y; :: thesis: ( u is_independent_of PA,G implies All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G)) )
assume A1: u is_independent_of PA,G ; :: thesis: All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (All ((u 'xor' a),PA,G)) . z = TRUE or (u 'xor' (All (a,PA,G))) . z = TRUE )
assume A2: (All ((u 'xor' a),PA,G)) . z = TRUE ; :: thesis: (u 'xor' (All (a,PA,G))) . z = TRUE
A3: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def 6;
A4: ( 'not' FALSE = TRUE & (u 'xor' (All (a,PA,G))) . z = ((All (a,PA,G)) . z) 'xor' (u . z) ) by BVFUNC_1:def 5, MARGREL1:11;

per cases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) or ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ;

suppose ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) ) ; :: thesis: (u 'xor' (All (a,PA,G))) . z = TRUE

then A5: ( u . z = TRUE & a . z = TRUE ) by EQREL_1:def 6;
A6: FALSE '&' TRUE = FALSE by MARGREL1:12;
(u 'xor' a) . z = (a . z) 'xor' (u . z) by BVFUNC_1:def 5
.= FALSE by A5, A6, MARGREL1:11 ;
hence (u 'xor' (All (a,PA,G))) . z = TRUE by A2, A3, BVFUNC_1:def 16; :: thesis: verum

end;

suppose A7: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ; :: thesis: (u 'xor' (All (a,PA,G))) . z = TRUE

then consider x1 being Element of Y such that
A8: x1 in EqClass (z,(CompF (PA,G))) and
a . x1 <> TRUE ;
A9: u . x1 = TRUE by A7, A8;
A10: (All (a,PA,G)) . z = FALSE by A7, BVFUNC_1:def 16;
u . z = u . x1 by A1, A3, A8, BVFUNC_1:def 15;
then (u 'xor' (All (a,PA,G))) . z = TRUE 'or' FALSE by A4, A10, A9
.= TRUE by BINARITH:3 ;
hence (u 'xor' (All (a,PA,G))) . z = TRUE ; :: thesis: verum

end;

suppose ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ; :: thesis: (u 'xor' (All (a,PA,G))) . z = TRUE

then consider x1 being Element of Y such that
A11: x1 in EqClass (z,(CompF (PA,G))) and
A12: u . x1 <> TRUE ;

now :: thesis: (u 'xor' (All (a,PA,G))) . z = TRUE

per cases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE or ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ;

suppose A13: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ; :: thesis: (u 'xor' (All (a,PA,G))) . z = TRUE

u . z = u . x1 by A1, A3, A11, BVFUNC_1:def 15;
then A14: u . z = FALSE by A12, XBOOLEAN:def 3;
(All (a,PA,G)) . z = TRUE by A13, BVFUNC_1:def 16;
then (u 'xor' (All (a,PA,G))) . z = FALSE 'or' TRUE by A4, A14
.= TRUE by BINARITH:3 ;
hence (u 'xor' (All (a,PA,G))) . z = TRUE ; :: thesis: verum

end;

suppose ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; :: thesis: (u 'xor' (All (a,PA,G))) . z = TRUE

then consider x2 being Element of Y such that
A15: x2 in EqClass (z,(CompF (PA,G))) and
A16: a . x2 <> TRUE ;
A17: a . x2 = FALSE by A16, XBOOLEAN:def 3;
u . x1 = u . x2 by A1, A11, A15, BVFUNC_1:def 15;
then A18: u . x2 = FALSE by A12, XBOOLEAN:def 3;
(u 'xor' a) . x2 = (a . x2) 'xor' (u . x2) by BVFUNC_1:def 5
.= FALSE by A18, A17, MARGREL1:12 ;
hence (u 'xor' (All (a,PA,G))) . z = TRUE by A2, A15, BVFUNC_1:def 16; :: thesis: verum

end;

end;

end;

hence (u 'xor' (All (a,PA,G))) . z = TRUE ; :: thesis: verum

end;

end;