for T1, T2 being TopSpace st not T1 is empty & not T2 is empty holds
( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] )