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

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