let X be set ; :: thesis: Top (BoolePoset X) = X
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:81; :: thesis: verum