let GX be TopStruct ; :: thesis: Int ({} GX) = {} GX
{} GX = ([#] GX) ` by XBOOLE_1:37
.= (Cl (({} GX) ` )) ` by Th27 ;
hence Int ({} GX) = {} GX ; :: thesis: verum