let a, b be Point of ; :: thesis: ].a,b.[ is Subset of
A1: [.a,b.] is Subset of by BORSUK_1:83, XXREAL_2:def 12;
].a,b.[ c= [.a,b.] by XXREAL_1:25;
hence ].a,b.[ is Subset of by A1, XBOOLE_1:1; :: thesis: verum