for x being object holds (Xchi (A,X)) . x >= 0

proof

let x be object ; :: thesis: (Xchi (A,X)) . x >= 0

per cases ( x in X or not x in X ) ;

suppose L1: x in X ; :: thesis: (Xchi (A,X)) . x >= 0

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: (Xchi (A,X)) . x >= 0

hence (Xchi (A,X)) . x >= 0 by L1, DefXchi; :: thesis: verum

end;

suppose not x in A ; :: thesis: (Xchi (A,X)) . x >= 0

hence (Xchi (A,X)) . x >= 0 by L1, DefXchi; :: thesis: verum

end;

end;

end;

suppose not x in X ; :: thesis: (Xchi (A,X)) . x >= 0

then not x in dom (Xchi (A,X)) ;
hence (Xchi (A,X)) . x >= 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence Xchi (A,X) is nonnegative by SUPINF_2:51; :: thesis: verum