set X = the infinite disjoint_with_NAT set ;
take FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) ; :: thesis: ( FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is infinite & not FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is degenerated & FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is well_founded & FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is ECIW-strict & FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is free & FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is strict )
thus ( FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is infinite & not FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is degenerated & FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is well_founded & FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is ECIW-strict & FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is free & FreeUnivAlgNSG (ECIW-signature, the infinite disjoint_with_NAT set ) is strict ) ; :: thesis: verum