let X be non empty set ; 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) = A
let S be SigmaField of X; for A being Element of S
for r being Real st r > 0 holds
great_eq_dom ((Xchi (A,X)),r) = A
let A be Element of S; for r being Real st r > 0 holds
great_eq_dom ((Xchi (A,X)),r) = A
let r be Real; ( r > 0 implies great_eq_dom ((Xchi (A,X)),r) = A )
assume A1:
r > 0
; great_eq_dom ((Xchi (A,X)),r) = A
now for x being object st x in A holds
x in great_eq_dom ((Xchi (A,X)),r)let x be
object ;
( x in A implies x in great_eq_dom ((Xchi (A,X)),r) )assume A2:
x in A
;
x in great_eq_dom ((Xchi (A,X)),r)then
x in X
;
then A4:
x in dom (Xchi (A,X))
by FUNCT_2:def 1;
(Xchi (A,X)) . x = +infty
by A2, DefXchi;
then
r <= (Xchi (A,X)) . x
by XXREAL_0:3;
hence
x in great_eq_dom (
(Xchi (A,X)),
r)
by A4, MESFUNC1:def 14;
verum end;
then A5:
A c= great_eq_dom ((Xchi (A,X)),r)
;
then
great_eq_dom ((Xchi (A,X)),r) c= A
;
hence
great_eq_dom ((Xchi (A,X)),r) = A
by A5; verum