( 0. (ExField (x,o)) = 0. F & 1. (ExField (x,o)) = 1. F ) by Def8;
hence not ExField (x,o) is degenerated by STRUCT_0:def 8; :: thesis: verum