the carrier of (ComplRelStr R) = the carrier of R by Def8;
hence not the carrier of (ComplRelStr R) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum