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