[:X,Y:] c= [:X,Y:] ;
then reconsider R = [:X,Y:] as Relation of X,Y ;
rng R = Y ;
then R is onto by FUNCT_2:def 3;
hence ex b₁ being Relation of X,Y st b₁ is onto ; :: thesis: verum