take ConwayOne ; :: thesis: ConwayOne is positive
thus ConwayOne is positive ; :: thesis: verum