take Polygon (s,2) ; :: thesis: ( not Polygon (s,2) is zero & Polygon (s,2) is s -gonal )
thus ( not Polygon (s,2) is zero & Polygon (s,2) is s -gonal ) ; :: thesis: verum