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