defpred S₁[ Element of [:(M -neighbour ),(M -neighbour ):]] means ex V, Q being Element of M -neighbour st
( $1 = [V,Q] & V,Q is_dst v );
{ W where W is Element of [:(M -neighbour ),(M -neighbour ):] : S₁[W] } c= [:(M -neighbour ),(M -neighbour ):] from FRAENKEL:sch 10();
hence { W where W is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) } is Subset of [:(M -neighbour ),(M -neighbour ):] ; :: thesis: verum