let X be set ; :: thesis: Bottom (BoolePoset X) = {}
thus Bottom (BoolePoset X) = "\/" ({},(LattPOSet (BooleLatt X))) by YELLOW_0:def 11
.= "\/" ({},(BooleLatt X)) by YELLOW_0:29
.= Bottom (BooleLatt X) by LATTICE3:49
.= {} by LATTICE3:3 ; :: thesis: verum