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}

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

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})

then
((a -con_map) " {x}) /\ ((a -con_map) " {y}) = {}
by XBOOLE_0:def 1;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 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

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