consider d being Element of BOOLEAN such that
A1: Bin1 1 = <*d*> by FINSEQ_2:117;
1 in Seg 1 by FINSEQ_1:5;
then (Bin1 1) /. 1 = TRUE by BINARI_2:7;
hence Bin1 1 = <*TRUE *> by A1, FINSEQ_4:25; :: thesis: verum