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 :: thesis: for g being object holds not g in ((a -con_map) " {x}) /\ ((a -con_map) " {y})
assume ex g being object 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} by A2, XBOOLE_0:def 4;
A4: g in (a -con_map) " {y} by A2, XBOOLE_0:def 4;
(a -con_map) . g in {x} by A3, FUNCT_1:def 7;
then A5: (a -con_map) . g = x by TARSKI:def 1;
(a -con_map) . g in {y} by A4, FUNCT_1:def 7;
hence contradiction by A1, A5, 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