let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All (u '&' a),PA,G = u '&' (All a,PA,G)
let G be Subset of (PARTITIONS Y); :: thesis: for u, a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All (u '&' a),PA,G = u '&' (All a,PA,G)
let u, a be Element of Funcs Y,BOOLEAN ; :: thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
All (u '&' a),PA,G = u '&' (All a,PA,G)
let PA be a_partition of Y; :: thesis: ( u is_independent_of PA,G implies All (u '&' a),PA,G = u '&' (All a,PA,G) )
assume u is_independent_of PA,G ; :: thesis: All (u '&' a),PA,G = u '&' (All a,PA,G)
then A1: u is_dependent_of CompF PA,G by Def8;
A2: All (u '&' a),PA,G '<' u '&' (All a,PA,G)

proof

let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not (All (u '&' a),PA,G) . z = TRUE or (u '&' (All a,PA,G)) . z = TRUE )
assume A3: (All (u '&' a),PA,G) . z = TRUE ; :: thesis: (u '&' (All a,PA,G)) . z = TRUE
A4: for x being Element of Y st x in EqClass z,(CompF PA,G) holds
a . x = TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass z,(CompF PA,G) implies a . x = TRUE )
assume x in EqClass z,(CompF PA,G) ; :: thesis: a . x = TRUE
then A5: (u '&' a) . x = TRUE by A3, BVFUNC_1:def 19;
(u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def 21;
hence a . x = TRUE by A5, MARGREL1:45; :: thesis: verum

end;

A6: for x being Element of Y st x in EqClass z,(CompF PA,G) holds
u . x = TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass z,(CompF PA,G) implies u . x = TRUE )
assume x in EqClass z,(CompF PA,G) ; :: thesis: u . x = TRUE
then A7: (u '&' a) . x = TRUE by A3, BVFUNC_1:def 19;
(u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def 21;
hence u . x = TRUE by A7, MARGREL1:45; :: thesis: verum

end;

A8: (u '&' (All a,PA,G)) . z = (u . z) '&' ((All a,PA,G) . z) by MARGREL1:def 21;
A9: (All a,PA,G) . z = TRUE by A4, BVFUNC_1:def 19;
z in EqClass z,(CompF PA,G) by EQREL_1:def 8;
then u . z = TRUE by A6;
hence (u '&' (All a,PA,G)) . z = TRUE by A8, A9; :: thesis: verum

end;

u '&' (All a,PA,G) '<' All (u '&' a),PA,G

proof

let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not (u '&' (All a,PA,G)) . z = TRUE or (All (u '&' a),PA,G) . z = TRUE )
assume (u '&' (All a,PA,G)) . z = TRUE ; :: thesis: (All (u '&' a),PA,G) . z = TRUE
then (u . z) '&' ((All a,PA,G) . z) = TRUE by MARGREL1:def 21;
then A10: ( u . z = TRUE & (All a,PA,G) . z = TRUE ) by MARGREL1:45;
A11: ( z in EqClass z,(CompF PA,G) & EqClass z,(CompF PA,G) in CompF PA,G ) by EQREL_1:def 8;
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(u '&' a) . x = TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass z,(CompF PA,G) implies (u '&' a) . x = TRUE )
assume A12: x in EqClass z,(CompF PA,G) ; :: thesis: (u '&' a) . x = TRUE
then A13: a . x = TRUE by A10, BVFUNC_1:def 19;
u . x = u . z by A1, A11, A12, BVFUNC_1:def 18;
then (u '&' a) . x = TRUE '&' TRUE by A10, A13, MARGREL1:def 21
.= TRUE ;
hence (u '&' a) . x = TRUE ; :: thesis: verum

end;

hence (All (u '&' a),PA,G) . z = TRUE by BVFUNC_1:def 19; :: thesis: verum

end;

hence All (u '&' a),PA,G = u '&' (All a,PA,G) by A2, BVFUNC_1:18; :: thesis: verum