consider X being set ;
( BooleLatt X is complete & BooleLatt X is \/-distributive & BooleLatt X 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