theorem Th1: :: ANPROJ_8:1

( [1,1] in [:(Seg 3),(Seg 3):] & [1,2] in [:(Seg 3),(Seg 3):] & [1,3] in [:(Seg 3),(Seg 3):] & [2,1] in [:(Seg 3),(Seg 3):] & [2,2] in [:(Seg 3),(Seg 3):] & [2,3] in [:(Seg 3),(Seg 3):] & [3,1] in [:(Seg 3),(Seg 3):] & [3,2] in [:(Seg 3),(Seg 3):] & [3,3] in [:(Seg 3),(Seg 3):] )