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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )

A3: now :: thesis: ( ( 1 <= k & k + 1 <= len f & LSeg (f,k) is boundary ) or ( ( not 1 <= k or not k + 1 <= len f ) & LSeg (f,k) is boundary ) )

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 3;
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 3;
hence LSeg (f,k) is boundary ; :: thesis: verum

end;

end;

end;

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union { (LSeg (f,i2)) where i2 is 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 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 Nat : ( 1 <= i & i + 1 <= k ) } ) by TARSKI:def 4;
ex i being 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 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 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 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 Nat : ( 1 <= i2 & i2 + 1 <= k + 1 ) } implies R2 is boundary )
assume A6: R2 = union { (LSeg (f,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= k + 1 ) } ; :: thesis: R2 is boundary
A7: R3 \/ (LSeg (f,k)) c= R2

proof

let z be object ; :: 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 Nat : ( 1 <= i2 & i2 + 1 <= k ) } ) by TARSKI:def 4;
consider i2 being 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 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 :: thesis: z in R2

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 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 3; :: thesis: verum

end;

end;

end;

hence z in R2 ; :: thesis: verum

end;

end;

end;

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

proof

let z be object ; :: 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 Nat : ( 1 <= i2 & i2 + 1 <= k + 1 ) } ) by A6, TARSKI:def 4;
consider i2 being Nat such that
A14: x = LSeg (f,i2) and
A15: 1 <= i2 and
A16: i2 + 1 <= k + 1 by A13;

now :: thesis: ( ( i2 + 1 <= k & ( z in R3 or z in LSeg (f,k) ) ) or ( i2 + 1 > k & ( z in R3 or z in LSeg (f,k) ) ) )

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 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;
hence R2 is boundary by A5, A3, TOPS_1:49; :: thesis: verum

end;

end;

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= 0 ) } or z in {} )
assume z in union { (LSeg (f,i)) where i is 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 Nat : ( 1 <= i & i + 1 <= 0 ) } ) by TARSKI:def 4;
ex i being 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 Nat holds S₁[j] from NAT_1:sch 2(A18, A2);
hence L~ f is boundary by A1; :: thesis: verum