[#] (T | P) = P by Def5;
hence not the carrier of (T | P) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum