let G be Group; :: thesis: for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N
let N be normal Subgroup of G; :: thesis: Left_Cosets N = Right_Cosets N
thus Left_Cosets N c= Right_Cosets N :: according to XBOOLE_0:def 10 :: thesis: Right_Cosets N c= Left_Cosets N
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Left_Cosets N or x in Right_Cosets N )
assume x in Left_Cosets N ; :: thesis: x in Right_Cosets N
then consider a being Element of G such that
A1: x = a * N by GROUP_2:def 15;
x = N * a by A1, Th117;
hence x in Right_Cosets N by GROUP_2:def 16; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Right_Cosets N or x in Left_Cosets N )
assume x in Right_Cosets N ; :: thesis: x in Left_Cosets N
then consider a being Element of G such that
A2: x = N * a by GROUP_2:def 16;
x = a * N by A2, Th117;
hence x in Left_Cosets N by GROUP_2:def 15; :: thesis: verum