let T be Refinement of T1,T2; :: thesis: not T is empty
the carrier of T = the carrier of T2 \/ the carrier of T1 by Def6;
hence not the carrier of T is empty ; :: according to STRUCT_0:def 1 :: thesis: verum