set X = the set ;
( BooleLatt the set is complete & BooleLatt the set is \/-distributive & BooleLatt the set is /\-distributive ) by Th26, Th27;
hence ex b₁ being Lattice st
( b₁ is complete & b₁ is \/-distributive & b₁ is /\-distributive & b₁ is strict ) ; :: thesis: verum