for M being non empty Reflexive symmetric triangle MetrStruct
for X, Y being Subset of M st the carrier of M = X \/ Y & not M is bounded & X is bounded holds
not Y is bounded