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) = A
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) = A
let A be Element of S; :: thesis: for r being Real st r > 0 holds
great_eq_dom ((Xchi (A,X)),r) = A
let r be Real; :: thesis: ( r > 0 implies great_eq_dom ((Xchi (A,X)),r) = A )
assume A1: r > 0 ; :: thesis: great_eq_dom ((Xchi (A,X)),r) = A
now :: thesis: for x being object st x in A holds
x in great_eq_dom ((Xchi (A,X)),r)
let x be object ; :: thesis: ( x in A implies x in great_eq_dom ((Xchi (A,X)),r) )
assume A2: x in A ; :: thesis: 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; :: thesis: verum
end;
then A5: A c= great_eq_dom ((Xchi (A,X)),r) ;
now :: thesis: for x being object st x in great_eq_dom ((Xchi (A,X)),r) holds
x in A
let x be object ; :: thesis: ( x in great_eq_dom ((Xchi (A,X)),r) implies x in A )
assume x in great_eq_dom ((Xchi (A,X)),r) ; :: thesis: x in A
then ( x in dom (Xchi (A,X)) & r <= (Xchi (A,X)) . x ) by MESFUNC1:def 14;
hence x in A by A1, DefXchi; :: thesis: verum
end;
then great_eq_dom ((Xchi (A,X)),r) c= A ;
hence great_eq_dom ((Xchi (A,X)),r) = A by A5; :: thesis: verum