let A, B be Subset of (TOP-REAL 2); :: thesis: for s being Real st A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s holds

proj1 .: A misses proj1 .: B

let s be Real; :: thesis: ( A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s implies proj1 .: A misses proj1 .: B )

assume that

A1: A misses B and

A2: A c= Horizontal_Line s and

A3: B c= Horizontal_Line s ; :: thesis: proj1 .: A misses proj1 .: B

assume proj1 .: A meets proj1 .: B ; :: thesis: contradiction

then consider e being object such that

A4: e in proj1 .: A and

A5: e in proj1 .: B by XBOOLE_0:3;

reconsider e = e as Real by A4;

consider d being Point of (TOP-REAL 2) such that

A6: d in B and

A7: e = proj1 . d by A5, FUNCT_2:65;

A8: d `2 = s by A3, A6, JORDAN6:32;

consider c being Point of (TOP-REAL 2) such that

A9: c in A and

A10: e = proj1 . c by A4, FUNCT_2:65;

c `2 = s by A2, A9, JORDAN6:32;

then c = |[(c `1),(d `2)]| by A8, EUCLID:53

.= |[e,(d `2)]| by A10, PSCOMP_1:def 5

.= |[(d `1),(d `2)]| by A7, PSCOMP_1:def 5

.= d by EUCLID:53 ;

hence contradiction by A1, A9, A6, XBOOLE_0:3; :: thesis: verum

proj1 .: A misses proj1 .: B

let s be Real; :: thesis: ( A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s implies proj1 .: A misses proj1 .: B )

assume that

A1: A misses B and

A2: A c= Horizontal_Line s and

A3: B c= Horizontal_Line s ; :: thesis: proj1 .: A misses proj1 .: B

assume proj1 .: A meets proj1 .: B ; :: thesis: contradiction

then consider e being object such that

A4: e in proj1 .: A and

A5: e in proj1 .: B by XBOOLE_0:3;

reconsider e = e as Real by A4;

consider d being Point of (TOP-REAL 2) such that

A6: d in B and

A7: e = proj1 . d by A5, FUNCT_2:65;

A8: d `2 = s by A3, A6, JORDAN6:32;

consider c being Point of (TOP-REAL 2) such that

A9: c in A and

A10: e = proj1 . c by A4, FUNCT_2:65;

c `2 = s by A2, A9, JORDAN6:32;

then c = |[(c `1),(d `2)]| by A8, EUCLID:53

.= |[e,(d `2)]| by A10, PSCOMP_1:def 5

.= |[(d `1),(d `2)]| by A7, PSCOMP_1:def 5

.= d by EUCLID:53 ;

hence contradiction by A1, A9, A6, XBOOLE_0:3; :: thesis: verum