let f be FinSequence of (TOP-REAL 2); for p, q being Point of (TOP-REAL 2) holds B_Cut (f,p,q) <> {}
let p, q be Point of (TOP-REAL 2); B_Cut (f,p,q) <> {}
A1:
R_Cut ((L_Cut (f,q)),p) <> {}
by JORDAN1J:44;
per cases
( ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) or ( not ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) )
;
suppose
( (
p in L~ f &
q in L~ f &
Index (
p,
f)
< Index (
q,
f) ) or (
Index (
p,
f)
= Index (
q,
f) &
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1) ) )
;
B_Cut (f,p,q) <> {} end; suppose
( not (
p in L~ f &
q in L~ f &
Index (
p,
f)
< Index (
q,
f) ) & not (
Index (
p,
f)
= Index (
q,
f) &
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1) ) )
;
B_Cut (f,p,q) <> {} end; end;