take A = FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ; :: thesis: ( A is Euclidean & not A is degenerated )
thus ( A is Euclidean & not A is degenerated ) ; :: thesis: verum