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