let a, b be Real; :: thesis: ( ( for s being Element of D holds a = Prob (judgefunc,s) ) & ( for s being Element of D holds b = Prob (judgefunc,s) ) implies a = b )
defpred S1[ Real] means for s being Element of D holds $1 = Prob (judgefunc,s);
assume A1: S1[a] ; :: thesis: ( ex s being Element of D st not b = Prob (judgefunc,s) or a = b )
assume A2: S1[b] ; :: thesis: a = b
now :: thesis: for s being Element of D holds a = b
let s be Element of D; :: thesis: a = b
( a = Prob (judgefunc,s) & b = Prob (judgefunc,s) ) by A1, A2;
hence a = b ; :: thesis: verum
end;
hence a = b ; :: thesis: verum