deffunc H₁( set ) -> Element of X = the Element of X;
defpred S₁[ set ] means X in X \ {{}};
{ [x,H₁(x)] where x is Element of X \ {{}} : S₁[x] } is Function from FOMODEL0:sch 3();
hence ( ChoiceOn X is Relation-like & ChoiceOn X is Function-like ) ; :: thesis: verum