theorem Th7: :: SGRAPH1:7

for A, e being set holds
( e in TWOELEMENTSETS A iff ex z being Subset of A st
( e = z & card z = 2 ) ) ;