let X be non empty set ; :: thesis: for S being SigmaField of X
for A being Element of S
for r being Real st r <= 0 holds
great_eq_dom ((Xchi (A,X)),r) = X
let S be SigmaField of X; :: thesis: for A being Element of S
for r being Real st r <= 0 holds
great_eq_dom ((Xchi (A,X)),r) = X
let A be Element of S; :: thesis: for r being Real st r <= 0 holds
great_eq_dom ((Xchi (A,X)),r) = X
let r be Real; :: thesis: ( r <= 0 implies great_eq_dom ((Xchi (A,X)),r) = X )
assume A1: r <= 0 ; :: thesis: great_eq_dom ((Xchi (A,X)),r) = X

now :: thesis: for x being object st x in X holds
x in great_eq_dom ((Xchi (A,X)),r)

let x be object ; :: thesis: ( x in X implies b₁ in great_eq_dom ((Xchi (A,X)),r) )
assume A2: x in X ; :: thesis: b₁ in great_eq_dom ((Xchi (A,X)),r)
then A3: x in dom (Xchi (A,X)) by FUNCT_2:def 1;

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

suppose x in A ; :: thesis: b₁ in great_eq_dom ((Xchi (A,X)),r)

then (Xchi (A,X)) . x = +infty by DefXchi;
then r <= (Xchi (A,X)) . x by XXREAL_0:3;
hence x in great_eq_dom ((Xchi (A,X)),r) by A3, MESFUNC1:def 14; :: thesis: verum

end;

suppose not x in A ; :: thesis: b₁ in great_eq_dom ((Xchi (A,X)),r)

then (Xchi (A,X)) . x = 0 by A2, DefXchi;
hence x in great_eq_dom ((Xchi (A,X)),r) by A1, A3, MESFUNC1:def 14; :: thesis: verum

end;

end;

end;

then X c= great_eq_dom ((Xchi (A,X)),r) ;
hence great_eq_dom ((Xchi (A,X)),r) = X ; :: thesis: verum