let Y be non empty set ; :: thesis: for a being constant Function of Y,BOOLEAN holds a is_dependent_of %O Y
let a be constant Function of Y,BOOLEAN; :: thesis: a is_dependent_of %O Y
for F being set st F in %O Y holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2

proof

let F be set ; :: thesis: ( F in %O Y implies for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 )
for x1, x2 being Element of Y holds a . x1 = a . x2

proof

let x1, x2 be Element of Y; :: thesis: a . x1 = a . x2

per cases ( a = O_el Y or a = I_el Y ) by Th20;

suppose A1: a = O_el Y ; :: thesis: a . x1 = a . x2

then a . x1 = FALSE by Def10;
hence a . x1 = a . x2 by A1, Def10; :: thesis: verum

end;

suppose A2: a = I_el Y ; :: thesis: a . x1 = a . x2

then a . x1 = TRUE by Def11;
hence a . x1 = a . x2 by A2, Def11; :: thesis: verum

end;

end;

end;

hence ( F in %O Y implies for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 ) ; :: thesis: verum

end;

hence a is_dependent_of %O Y ; :: thesis: verum