let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: 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
let X, Y be Subset of M; :: thesis: ( the carrier of M = X \/ Y & not M is bounded & X is bounded implies not Y is bounded )
assume that
A1: the carrier of M = X \/ Y and
A2: not M is bounded ; :: thesis: ( not X is bounded or not Y is bounded )
assume ( X is bounded & Y is bounded ) ; :: thesis: contradiction
then [#] M is bounded by A1, TBSP_1:20;
hence contradiction by A2, TBSP_1:25; :: thesis: verum