theorem Th28: :: CARDFIL4:33

for i, j being Nat ex n being Nat st square-uparrow n c= [:(NAT \ (Segm i)),(NAT \ (Segm j)):]