the carrier of (IsomGroup n) = ISOM (RLMSpace n) by Def9;
hence not IsomGroup n is empty ; :: thesis: verum