Z_3 is finite by MOD_2:def 20;
hence ex b₁ being Field st
( b₁ is strict & b₁ is finite ) by MOD_2:27; :: thesis: verum