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 ( x in {} & y in {} ) ; :: thesis: [x,y] in T
hence [x,y] in T ; :: thesis: verum