let f be FinSequence of (TOP-REAL 2); :: thesis: L~ f is boundary
A1: L~ f = union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TOPREAL1:def 6;
defpred S₁[ Element of NAT ] means for R1 being Subset of (TOP-REAL 2) st R1 = union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= $1 ) } holds
R1 is boundary ;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )

A3: now

per cases ( ( 1 <= k & k + 1 <= len f ) or not 1 <= k or not k + 1 <= len f ) ;

case ( 1 <= k & k + 1 <= len f ) ; :: thesis: LSeg f,k is boundary

then LSeg f,k = LSeg (f /. k),(f /. (k + 1)) by TOPREAL1:def 5;
hence LSeg f,k is boundary ; :: thesis: verum

end;

case ( not 1 <= k or not k + 1 <= len f ) ; :: thesis: LSeg f,k is boundary

then LSeg f,k = {} by TOPREAL1:def 5;
hence LSeg f,k is boundary ; :: thesis: verum

end;

end;

end;

union { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k ) } c= the carrier of (TOP-REAL 2)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in union { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k ) } or z in the carrier of (TOP-REAL 2) )
assume z in union { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k ) } ; :: thesis: z in the carrier of (TOP-REAL 2)
then consider x being set such that
A4: ( z in x & x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= k ) } ) by TARSKI:def 4;
ex i being Element of NAT st
( x = LSeg f,i & 1 <= i & i + 1 <= k ) by A4;
hence z in the carrier of (TOP-REAL 2) by A4; :: thesis: verum

end;

then reconsider R3 = union { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k ) } as Subset of (TOP-REAL 2) ;
assume for R1 being Subset of (TOP-REAL 2) st R1 = union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= k ) } holds
R1 is boundary ; :: thesis: S₁[k + 1]
then A5: R3 is boundary ;
thus for R2 being Subset of (TOP-REAL 2) st R2 = union { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k + 1 ) } holds
R2 is boundary :: thesis: verum

proof

let R2 be Subset of (TOP-REAL 2); :: thesis: ( R2 = union { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k + 1 ) } implies R2 is boundary )
assume A6: R2 = union { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k + 1 ) } ; :: thesis: R2 is boundary
A7: R3 \/ (LSeg f,k) c= R2

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in R3 \/ (LSeg f,k) or z in R2 )
assume A8: z in R3 \/ (LSeg f,k) ; :: thesis: z in R2

per cases ( z in R3 or z in LSeg f,k ) by A8, XBOOLE_0:def 3;

suppose z in R3 ; :: thesis: z in R2

then consider x being set such that
A9: ( z in x & x in { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k ) } ) by TARSKI:def 4;
consider i2 being Element of NAT such that
A10: ( x = LSeg f,i2 & 1 <= i2 ) and
A11: i2 + 1 <= k by A9;
i2 + 1 < k + 1 by A11, NAT_1:13;
then x in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= k + 1 ) } by A10;
hence z in R2 by A6, A9, TARSKI:def 4; :: thesis: verum

end;

suppose A12: z in LSeg f,k ; :: thesis: z in R2

now

per cases ( 1 <= k or k < 1 ) ;

suppose 1 <= k ; :: thesis: z in R2

then LSeg f,k in { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k + 1 ) } ;
hence z in R2 by A6, A12, TARSKI:def 4; :: thesis: verum

end;

suppose k < 1 ; :: thesis: z in R2

hence z in R2 by A12, TOPREAL1:def 5; :: thesis: verum

end;

end;

end;

hence z in R2 ; :: thesis: verum

end;

end;

end;

R2 c= R3 \/ (LSeg f,k)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in R2 or z in R3 \/ (LSeg f,k) )
assume z in R2 ; :: thesis: z in R3 \/ (LSeg f,k)
then consider x being set such that
A13: ( z in x & x in { (LSeg f,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= k + 1 ) } ) by A6, TARSKI:def 4;
consider i2 being Element of NAT such that
A14: x = LSeg f,i2 and
A15: 1 <= i2 and
A16: i2 + 1 <= k + 1 by A13;

now

per cases ( i2 + 1 <= k or i2 + 1 > k ) ;

case i2 + 1 <= k ; :: thesis: ( z in R3 or z in LSeg f,k )

then x in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= k ) } by A14, A15;
hence ( z in R3 or z in LSeg f,k ) by A13, TARSKI:def 4; :: thesis: verum

end;

case i2 + 1 > k ; :: thesis: ( z in R3 or z in LSeg f,k )

then k + 1 <= i2 + 1 by NAT_1:13;
then i2 + 1 = k + 1 by A16, XXREAL_0:1;
hence ( z in R3 or z in LSeg f,k ) by A13, A14; :: thesis: verum

end;

end;

end;

hence z in R3 \/ (LSeg f,k) by XBOOLE_0:def 3; :: thesis: verum

end;

then R2 = R3 \/ (LSeg f,k) by A7, XBOOLE_0:def 10;
hence R2 is boundary by A5, A3, TOPS_1:85; :: thesis: verum

end;

end;

union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= 0 ) } c= {}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= 0 ) } or z in {} )
assume z in union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= 0 ) } ; :: thesis: z in {}
then consider x being set such that
A17: ( z in x & x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= 0 ) } ) by TARSKI:def 4;
ex i being Element of NAT st
( x = LSeg f,i & 1 <= i & i + 1 <= 0 ) by A17;
hence z in {} ; :: thesis: verum

end;

then A18: S₁[ 0 ] ;
for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A18, A2);
hence L~ f is boundary by A1; :: thesis: verum