let A, B be Subset of (TOP-REAL 2); :: thesis: for s being real number st A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s holds
proj1 .: A misses proj1 .: B
let s be real number ; :: 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 set 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 c being Point of (TOP-REAL 2) such that
A6: c in A and
A7: e = proj1 . c by A4, FUNCT_2:116;
consider d being Point of (TOP-REAL 2) such that
A8: d in B and
A9: e = proj1 . d by A5, FUNCT_2:116;
( c `2 = s & d `2 = s ) by A2, A3, A6, A8, JORDAN6:35;
then c = |[(c `1 ),(d `2 )]| by EUCLID:57
.= |[e,(d `2 )]| by A7, PSCOMP_1:def 28
.= |[(d `1 ),(d `2 )]| by A9, PSCOMP_1:def 28
.= d by EUCLID:57 ;
hence contradiction by A1, A6, A8, XBOOLE_0:3; :: thesis: verum