| apply (. (#‡e1)‡(e‡#)); assumption]]
qed.
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun21 (concr _) __ (relS _) x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun21 ___ (relS _)).
+interpretation "basic pair relation for subsets" 'Vdash2 x y c = (fun21 (concr _) __ (relS c) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash c = (fun21 ___ (relS c)).