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