theorem :: BROUWER:1

for S, T being non empty TopSpace
for x being set holds
( x in DiffElems (S,T) iff ex s being Point of S ex t being Point of T st
( x = [s,t] & s <> t ) ) ;