{} GX = ([#] GX) ` by XBOOLE_1:37
.= (Cl (({} GX) `)) ` by Th2 ;
hence Int ({} GX) is empty ; :: thesis: verum