let a be set ; :: thesis: {a} is mutually-disjoint

let x, y be set ; :: according to TAXONOM2:def 5 :: thesis: ( x in {a} & y in {a} & x <> y implies x misses y )

assume that

A1: x in {a} and

A2: y in {a} and

A3: x <> y ; :: thesis: x misses y

x = a by A1, TARSKI:def 1;

hence x misses y by A2, A3, TARSKI:def 1; :: thesis: verum

let x, y be set ; :: according to TAXONOM2:def 5 :: thesis: ( x in {a} & y in {a} & x <> y implies x misses y )

assume that

A1: x in {a} and

A2: y in {a} and

A3: x <> y ; :: thesis: x misses y

x = a by A1, TARSKI:def 1;

hence x misses y by A2, A3, TARSKI:def 1; :: thesis: verum