let A, B be non empty compact Subset of REAL; :: thesis: ( A misses B implies dist (A,B) > 0 )
assume A1: A misses B ; :: thesis: dist (A,B) > 0
consider r0, s0 being real number such that
A2: r0 in A and
A3: s0 in B and
A4: dist (A,B) = abs (r0 - s0) by Th18;
reconsider r0 = r0, s0 = s0 as Real by XREAL_0:def 1;
assume dist (A,B) <= 0 ; :: thesis: contradiction
then abs (r0 - s0) = 0 by A4, Th19;
then r0 = s0 by GOBOARD7:2;
hence contradiction by A1, A2, A3, XBOOLE_0:3; :: thesis: verum