take {} ; :: thesis: not {} is pair
let x, y be set ; :: according to FACIRC_1:def 1 :: thesis: not {} = [x,y]
thus not {} = [x,y] ; :: thesis: verum