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