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