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