let X be set ; :: thesis: for x being object st ex u, v being object st
( u <> v & u in X & v in X ) holds
X \ {x} <> {}
let x be object ; :: thesis: ( ex u, v being object st
( u <> v & u in X & v in X ) implies X \ {x} <> {} )
assume A1: ex u, v being object st
( u <> v & u in X & v in X ) ; :: thesis: X \ {x} <> {}
assume A2: not X \ {x} <> {} ; :: thesis: contradiction
A3: now :: thesis: for z being object st z in X holds
z = x
let z be object ; :: thesis: ( z in X implies z = x )
assume A4: z in X ; :: thesis: z = x
( not z in X or z in {x} ) by XBOOLE_0:def 5, A2;
hence z = x by TARSKI:def 1, A4; :: thesis: verum
end;
consider u, v being object such that
A5: ( u <> v & u in X & v in X ) by A1;
( u = x & v = x ) by A5, A3;
hence contradiction by A5; :: thesis: verum