deffunc H₁( set , set ) -> set = $1 /\ $2;
let f, g be FinSequence of (TOP-REAL 2); :: thesis: INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) is finite
set AL = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set BL = { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ;
set IN = { H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) } ;
A1: { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } is finite by SPPOL_1:45;
set C = INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } );
A2: { H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) } c= INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } )

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) } or a in INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) )
assume a in { H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) } ; :: thesis: a in INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } )
then ex X, Y being Subset of (TOP-REAL 2) st
( a = X /\ Y & X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) ;
hence a in INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) by SETFAM_1:def 5; :: thesis: verum

end;

A3: INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) c= { H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) or a in { H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) } )
assume a in INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) ; :: thesis: a in { H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) }
then consider X, Y being set such that
A4: ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) and
A5: a = X /\ Y by SETFAM_1:def 5;
( ex i being Element of NAT st
( X = LSeg (f,i) & 1 <= i & i + 1 <= len f ) & ex j being Element of NAT st
( Y = LSeg (g,j) & 1 <= j & j + 1 <= len g ) ) by A4;
then reconsider X = X, Y = Y as Subset of (TOP-REAL 2) ;
X /\ Y in { H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) } by A4;
hence a in { H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) } by A5; :: thesis: verum

end;

A6: { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is finite by SPPOL_1:45;
{ H₁(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) } is finite from FRAENKEL:sch 22(A6, A1);
hence INTERSECTION ( { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) is finite by A2, A3, XBOOLE_0:def 10; :: thesis: verum