let A, B be non empty compact Subset of REAL; ( A misses B implies dist (A,B) > 0 )
assume A1:
A misses B
; 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
; contradiction
then
|.(r0 - s0).| = 0
by A4, Th10;
then
r0 = s0
by GOBOARD7:2;
hence
contradiction
by A1, A2, A3, XBOOLE_0:3; verum