take [0 ,1] ; :: thesis: [0 ,1] is pair
take 0 ; :: according to FACIRC_1:def 1 :: thesis: ex y being set st [0 ,1] = [0 ,y]
take 1 ; :: thesis: [0 ,1] = [0 ,1]
thus [0 ,1] = [0 ,1] ; :: thesis: verum