theorem :: SURREALO:30
for X, Y being set st X c= Y holds
X <=_ Y ;