for x being object holds (chi (A,B)) . x >= 0
proof
let x be object ; :: thesis: (chi (A,B)) . x >= 0
per cases ( ( x in B & x in A ) or ( x in B & not x in A ) or not x in B ) ;
suppose ( x in B & x in A ) ; :: thesis: (chi (A,B)) . x >= 0
hence (chi (A,B)) . x >= 0 by FUNCT_3:def 3; :: thesis: verum
end;
suppose ( x in B & not x in A ) ; :: thesis: (chi (A,B)) . x >= 0
hence (chi (A,B)) . x >= 0 by FUNCT_3:def 3; :: thesis: verum
end;
suppose not x in B ; :: thesis: (chi (A,B)) . x >= 0
then not x in dom (chi (A,B)) ;
hence (chi (A,B)) . x >= 0 by FUNCT_1:def 2; :: thesis: verum
end;
end;
end;
hence chi (A,B) is nonnegative by SUPINF_2:51; :: thesis: verum