theorem Th30: :: CARDFIL4:35

for n being Nat holds square-downarrow n = [:(Segm n),(Segm n):]