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