let S be non empty finite set ; :: thesis: for D being Element of distribution_family S holds
( not D is well-distributed iff D = {(<*> S)} )
let D be Element of distribution_family S; :: thesis: ( not D is well-distributed iff D = {(<*> S)} )
thus ( not D is well-distributed implies D = {(<*> S)} ) :: thesis: ( D = {(<*> S)} implies not D is well-distributed )

proof

assume not D is well-distributed ; :: thesis: D = {(<*> S)}
then reconsider o = {} as Element of D by SETFAM_1:def 8;
A1: for s being Element of D holds
( s in {(<*> S)} & s = <*> S )

proof

let s be Element of D; :: thesis: ( s in {(<*> S)} & s = <*> S )
for x being set holds FDprobability (x,s) = 0

proof

let x be set ; :: thesis: FDprobability (x,s) = 0
FDprobability (x,s) = FDprobability (x,o) by Th4, DIST_1:def 4;
hence FDprobability (x,s) = 0 ; :: thesis: verum

end;

then s is empty by Th5;
hence ( s in {(<*> S)} & s = <*> S ) by TARSKI:def 1; :: thesis: verum

end;

then A2: for z being object st z in D holds
z in {(<*> S)} ;
for z being object st z in {(<*> S)} holds
z in D

proof

let z be object ; :: thesis: ( z in {(<*> S)} implies z in D )
assume A3: z in {(<*> S)} ; :: thesis: z in D
z is Element of D

proof

assume A4: z is not Element of D ; :: thesis: contradiction
set t = the Element of D;
the Element of D = <*> S by A1;
hence contradiction by A4, A3, TARSKI:def 1; :: thesis: verum

end;

hence z in D ; :: thesis: verum

end;

hence D = {(<*> S)} by A2, TARSKI:2; :: thesis: verum

end;

assume A5: D = {(<*> S)} ; :: thesis: not D is well-distributed
assume A6: D is well-distributed ; :: thesis: contradiction
set s = the Element of D;
the Element of D = {} by A5, TARSKI:def 1;
hence contradiction by A6; :: thesis: verum