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