theorem Th24: :: YELLOW13:24

for T being TopStruct holds bool the carrier of T is basis of T