let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & p <> q holds

B_Cut (f,p,q) is being_S-Seq

let p, q be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & q in L~ f & p <> q implies B_Cut (f,p,q) is being_S-Seq )

assume that

A1: f is being_S-Seq and

A2: p in L~ f and

A3: q in L~ f and

A4: p <> q ; :: thesis: B_Cut (f,p,q) is being_S-Seq

B_Cut (f,p,q) is_S-Seq_joining p,q by A1, A2, A3, A4, Th36;

hence B_Cut (f,p,q) is being_S-Seq ; :: thesis: verum

B_Cut (f,p,q) is being_S-Seq

let p, q be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & q in L~ f & p <> q implies B_Cut (f,p,q) is being_S-Seq )

assume that

A1: f is being_S-Seq and

A2: p in L~ f and

A3: q in L~ f and

A4: p <> q ; :: thesis: B_Cut (f,p,q) is being_S-Seq

B_Cut (f,p,q) is_S-Seq_joining p,q by A1, A2, A3, A4, Th36;

hence B_Cut (f,p,q) is being_S-Seq ; :: thesis: verum