the carrier of (Omega T) = the carrier of T by Lm1;
hence the carrier of (Omega T) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum