:: Formalization of Ortholattices via Orthoposets :: by Adam Grabowski and Markus Moschner :: :: Received December 28, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users
begin
:: Originally proved by McCune with the help of OTTER
:: Axiomatics for ortholattices is the classical one for lattices extended
:: by the three following:
:: x ^ y = c(c(x) v c(y)). % DM de_Morgan from ROBBINS1
:: c(c(x)) = x. % CC involutive from OPOSET_1, too specific
:: x v c(x) = y v c(y). % ONE