deffunc H_{1}( set , set ) -> set = $1 /\ $2;

let f, g be FinSequence of (TOP-REAL 2); :: thesis: INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) is finite

set AL = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;

set BL = { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ;

set IN = { H_{1}(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) } ;

A1: { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } is finite by SPPOL_1:23;

set C = INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } );

A2: INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) c= { H_{1}(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) }

{ H_{1}(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) } is finite
from FRAENKEL:sch 22(A5, A1);

hence INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) is finite by A2; :: thesis: verum

let f, g be FinSequence of (TOP-REAL 2); :: thesis: INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) is finite

set AL = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;

set BL = { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ;

set IN = { H

A1: { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } is finite by SPPOL_1:23;

set C = INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } );

A2: INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) c= { H

proof

A5:
{ (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } is finite
by SPPOL_1:23;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) or a in { H_{1}(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) } )

assume a in INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) ; :: thesis: a in { H_{1}(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) }

then consider X, Y being set such that

A3: ( X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) and

A4: a = X /\ Y by SETFAM_1:def 5;

( ex i being Nat st

( X = LSeg (f,i) & 1 <= i & i + 1 <= len f ) & ex j being Nat st

( Y = LSeg (g,j) & 1 <= j & j + 1 <= len g ) ) by A3;

then reconsider X = X, Y = Y as Subset of (TOP-REAL 2) ;

X /\ Y in { H_{1}(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) }
by A3;

hence a in { H_{1}(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) }
by A4; :: thesis: verum

end;assume a in INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) ; :: thesis: a in { H

then consider X, Y being set such that

A3: ( X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) and

A4: a = X /\ Y by SETFAM_1:def 5;

( ex i being Nat st

( X = LSeg (f,i) & 1 <= i & i + 1 <= len f ) & ex j being Nat st

( Y = LSeg (g,j) & 1 <= j & j + 1 <= len g ) ) by A3;

then reconsider X = X, Y = Y as Subset of (TOP-REAL 2) ;

X /\ Y in { H

hence a in { H

{ H

hence INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) is finite by A2; :: thesis: verum