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 that
A3: X is bounded and
A4: Y is bounded ; :: thesis: contradiction
[#] M is bounded by A1, A3, A4, TBSP_1:13;
hence contradiction by A2, TBSP_1:18; :: thesis: verum