let X be set ; :: thesis: Top (BoolePoset X) = X
X in bool X by ZFMISC_1:def 1;
then union (bool X) in bool X by ZFMISC_1:99;
then A1: Top (InclPoset (bool X)) = union (bool X) by Th14;
BoolePoset X = InclPoset (bool X) by Th4;
hence Top (BoolePoset X) = X by A1, ZFMISC_1:99; :: thesis: verum