/* * There exists a surjection from S to T iff S has more elements than T. */ MACHINE SurjEx INCLUDES DomRan, PermEx ASSERTIONS !(ss, tt) . (ss : FIN1(INTEGER) & tt : FIN1(INTEGER) => ((card(ss) >= card(tt)) <=> ((ss -->> tt) /= {}))) END