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 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