let G be Group; :: thesis: for a being Element of G
for x, y being Element of con_class a st x <> y holds
(a -con_map ) " {x} misses (a -con_map ) " {y}
let a be Element of G; :: thesis: for x, y being Element of con_class a st x <> y holds
(a -con_map ) " {x} misses (a -con_map ) " {y}
let x, y be Element of con_class a; :: thesis: ( x <> y implies (a -con_map ) " {x} misses (a -con_map ) " {y} )
assume A1: x <> y ; :: thesis: (a -con_map ) " {x} misses (a -con_map ) " {y}

now

assume ex g being set st g in ((a -con_map ) " {x}) /\ ((a -con_map ) " {y}) ; :: thesis: contradiction
then consider g being set such that
A2: g in ((a -con_map ) " {x}) /\ ((a -con_map ) " {y}) ;
A3: ( g in (a -con_map ) " {x} & g in (a -con_map ) " {y} ) by A2, XBOOLE_0:def 4;
then (a -con_map ) . g in {x} by FUNCT_1:def 13;
then A4: (a -con_map ) . g = x by TARSKI:def 1;
(a -con_map ) . g in {y} by A3, FUNCT_1:def 13;
hence contradiction by A1, A4, TARSKI:def 1; :: thesis: verum

end;

then ((a -con_map ) " {x}) /\ ((a -con_map ) " {y}) = {} by XBOOLE_0:def 1;
hence (a -con_map ) " {x} misses (a -con_map ) " {y} by XBOOLE_0:def 7; :: thesis: verum