let X be set ; :: thesis: the carrier of (BoolePoset X) = bool X
set L = BoolePoset X;
BoolePoset X = InclPoset (bool X) by YELLOW_1:4;
then BoolePoset X = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def 1;
hence the carrier of (BoolePoset X) = bool X ; :: thesis: verum