let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_SUP (a,PA) is_dependent_of PA
let a be Function of Y,BOOLEAN; :: thesis: for PA being a_partition of Y holds B_SUP (a,PA) is_dependent_of PA
let PA be a_partition of Y; :: thesis: B_SUP (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_SUP (a,PA)) . x1 = (B_SUP (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_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2 )
assume A1: F in PA ; :: thesis: for x1, x2 being set st x1 in F & x2 in F holds
(B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2
let x1, x2 be set ; :: thesis: ( x1 in F & x2 in F implies (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2 )
assume A2: ( x1 in F & x2 in F ) ; :: thesis: (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2
then reconsider x1 = x1, x2 = x2 as Element of Y by A1;
A3: x1 in EqClass (x1,PA) by EQREL_1:def 6;
( EqClass (x1,PA) = F or EqClass (x1,PA) misses F ) by A1, EQREL_1:def 4;
then A4: EqClass (x2,PA) = EqClass (x1,PA) by A2, A3, EQREL_1:def 6, XBOOLE_0:3;
per cases ( ex x being Element of Y st
( x in EqClass (x1,PA) & a . x = TRUE ) or for x being Element of Y holds
( not x in EqClass (x1,PA) or not a . x = TRUE ) ) ;
suppose A5: ex x being Element of Y st
( x in EqClass (x1,PA) & a . x = TRUE ) ; :: thesis: (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2
then (B_SUP (a,PA)) . x1 = TRUE by Def17;
hence (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2 by A4, A5, Def17; :: thesis: verum
end;
suppose A6: for x being Element of Y holds
( not x in EqClass (x1,PA) or not a . x = TRUE ) ; :: thesis: (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2
then (B_SUP (a,PA)) . x1 = FALSE by Def17;
hence (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2 by A4, A6, Def17; :: thesis: verum
end;
end;
end;
hence B_SUP (a,PA) is_dependent_of PA ; :: thesis: verum