take ConwayZero ; :: thesis: ( ConwayZero is left-right & ConwayZero is strict )
thus ( ConwayZero is left-right & ConwayZero is strict ) ; :: thesis: verum