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