( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
hence ( [1,1] in [:(Seg 1),(Seg 3):] & [1,2] in [:(Seg 1),(Seg 3):] & [1,3] in [:(Seg 1),(Seg 3):] ) by ZFMISC_1:87; :: thesis: verum