( 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 3),(Seg 1):] & [2,1] in [:(Seg 3),(Seg 1):] & [3,1] in [:(Seg 3),(Seg 1):] ) by ZFMISC_1:87; :: thesis: verum