let A, B be non empty set ; for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.[ & A misses B & not q <= r holds
s <= p
let p, q, r, s be R_eal; ( A = ].p,q.] & B = ].r,s.[ & A misses B & not q <= r implies s <= p )
assume that
A1:
A = ].p,q.]
and
A2:
B = ].r,s.[
and
A3:
A misses B
; ( q <= r or s <= p )
assume A4:
( q > r & s > p )
; contradiction