let G be addGroup; :: thesis: for a being Element of G
for H being finite Subgroup of G ex B, C being finite set st
( B = a + H & C = H + a & card H = card B & card H = card C )
let a be Element of G; :: thesis: for H being finite Subgroup of G ex B, C being finite set st
( B = a + H & C = H + a & card H = card B & card H = card C )
let H be finite Subgroup of G; :: thesis: ex B, C being finite set st
( B = a + H & C = H + a & card H = card B & card H = card C )
reconsider B = a + H, C = H + a as finite set by Th131, CARD_1:38;
take B ; :: thesis: ex C being finite set st
( B = a + H & C = H + a & card H = card B & card H = card C )
take C ; :: thesis: ( B = a + H & C = H + a & card H = card B & card H = card C )
thus ( B = a + H & C = H + a & card H = card B & card H = card C ) by Th131, CARD_1:5; :: thesis: verum