ド・モルガンの法則の半分

theorem half_DeMorgan
  premise h: ￢A∧￢B 
  entails ￢(A∨B)
proof
  we have not_a: ￢A by using And_left with h
  we have not_b: ￢B by using And_light with h
  we conclude ￢(A ∨ B) by using Or_tuple with not_a and not_b
end

定理 ド・モルガンの半分
  前提 h: ￢A∧￢B は
   ￢(A∨B) を帰結する。
証明
  And_left を h と共に使って、
  not_a: ￢A を得る。
  And_light を h と共に使って、
  not_b: ￢B を得る。
  Or_tuple を not_a と not_b と共に使って、
  我々は ￢(A ∨ B) を結論とする。
終わり