( 1 is square-free & 1 is square ) by SFS;
hence ex b₁ being Nat st
( b₁ is square-free & b₁ is square ) ; :: thesis: verum