set p = the Element of S;
( 1. (unionField (S,f,E)) = 1. ( the Element of S `1) & 0. (unionField (S,f,E)) = 0. ( the Element of S `1) ) by lem5a;
hence not unionField (S,f,E) is degenerated ; :: thesis: verum