let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: for k being Element of NAT holds { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2)
let k be Element of NAT ; :: thesis: { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2)
set F = { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } ;
{ (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } c= bool (REAL 2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } or x in bool (REAL 2) )
assume x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } ; :: thesis: x in bool (REAL 2)
then ex i being Element of NAT st
( LSeg f,i = x & 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) ;
then x is Subset of (REAL 2) by EUCLID:25;
hence x in bool (REAL 2) ; :: thesis: verum

end;

hence { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2) by EUCLID:25; :: thesis: verum