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