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