take {} ; :: thesis: for x, y being set st x in {} & y in {} holds
[x,y] in T
let x, y be set ; :: thesis: ( x in {} & y in {} implies [x,y] in T )
assume that
A1: x in {} and
y in {} ; :: thesis: [x,y] in T
thus [x,y] in T by A1; :: thesis: verum