let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds crossover p1,p2,0 ,0 ,0 ,0 = p1
let p1, p2 be Individual of S; :: thesis: crossover p1,p2,0 ,0 ,0 ,0 = p1
crossover p1,p2,0 ,0 ,0 ,0 = crossover p2,p1,0 by Th31;
hence crossover p1,p2,0 ,0 ,0 ,0 = p1 by Th4; :: thesis: verum