F_Real is Fanoian by Def31, Th78;
hence ex b₁ being Field st
( b₁ is strict & b₁ is Fanoian ) ; :: thesis: verum