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 such that
A2: r0 in A and
A3: s0 in B and
A4: dist (A,B) = |.(r0 - s0).| by Th9;
reconsider r0 = r0, s0 = s0 as Real ;
assume dist (A,B) <= 0 ; :: thesis: contradiction
then |.(r0 - s0).| = 0 by A4, Th10;
then r0 = s0 by GOBOARD7:2;
hence contradiction by A1, A2, A3, XBOOLE_0:3; :: thesis: verum