take {[0,{},{}],[1,{},{}]} ; :: thesis: not {[0,{},{}],[1,{},{}]} is trivial
[0,{},{}] <> [1,{},{}] by XTUPLE_0:3;
hence not {[0,{},{}],[1,{},{}]} is trivial by CHAIN_1:3; :: thesis: verum