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_{1} being Lattice st

( b_{1} is complete & b_{1} is \/-distributive & b_{1} is /\-distributive & b_{1} is strict )
; :: thesis: verum

( BooleLatt the set is complete & BooleLatt the set is \/-distributive & BooleLatt the set is /\-distributive ) by Th26, Th27;

hence ex b

( b