let Y be non empty set ; :: thesis: for a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds B_INF (a,PA) is_dependent_of PA
let a be Element of Funcs (Y,BOOLEAN); :: thesis: for PA being a_partition of Y holds B_INF (a,PA) is_dependent_of PA
let PA be a_partition of Y; :: thesis: B_INF (a,PA) is_dependent_of PA
for F being set st F in PA holds
for x1, x2 being set st x1 in F & x2 in F holds
(B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2

proof

let F be set ; :: thesis: ( F in PA implies for x1, x2 being set st x1 in F & x2 in F holds
(B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2 )
assume A1: F in PA ; :: thesis: for x1, x2 being set st x1 in F & x2 in F holds
(B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2
let x1, x2 be set ; :: thesis: ( x1 in F & x2 in F implies (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2 )
assume that
A2: x1 in F and
A3: x2 in F ; :: thesis: (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2
reconsider x1 = x1 as Element of Y by A1, A2;
A4: ( EqClass (x1,PA) = F or EqClass (x1,PA) misses F ) by A1, EQREL_1:def 4;
reconsider x2 = x2 as Element of Y by A1, A3;
x2 in EqClass (x2,PA) by EQREL_1:def 6;
then EqClass (x2,PA) meets F by A3, XBOOLE_0:3;
then A5: ( x1 in EqClass (x1,PA) & EqClass (x2,PA) = F ) by A1, EQREL_1:def 4, EQREL_1:def 6;

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

suppose A6: for x being Element of Y st x in EqClass (x1,PA) holds
a . x = TRUE ; :: thesis: (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2

then (B_INF (a,PA)) . x1 = TRUE by Def19;
hence (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2 by A2, A4, A5, A6, Def19, XBOOLE_0:3; :: thesis: verum

end;

suppose A7: ex x being Element of Y st
( x in EqClass (x1,PA) & not a . x = TRUE ) ; :: thesis: (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2

then (B_INF (a,PA)) . x1 = FALSE by Def19;
hence (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2 by A2, A4, A5, A7, Def19, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

hence B_INF (a,PA) is_dependent_of PA by Def18; :: thesis: verum