let G be finite addGroup; :: thesis:
let H be Subgroup of G; :: thesis:
reconsider C = Left_Cosets H as finite set ;

let X be set ; :: thesis:
assume A1: X in C ; :: thesis:
then reconsider x = X as Subset of G ;
x is finite ;
then reconsider B = X as finite set ;
take B = B; :: thesis:
thus B = X ; :: thesis:
consider a being Element of G such that
A2: x = a + H by A1, Def15;
ex B, C being finite set st
( B = a + H & C = H + a & card H = card B & card H = card C ) by Th133;
hence card B = card H by A2; :: thesis:
let Y be set ; :: thesis:
assume that
A3: Y in C and
A4: X <> Y ; :: thesis:
reconsider y = Y as Subset of G by A3;
A5: ex b being Element of G st y = b + H by A3, Def15;
hence X,Y are_equipotent by A2, Th128; :: thesis:
thus X misses Y by A2, A4, A5, Th115; :: thesis:

end;