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 ) } ;
deffunc H₁( set , set ) -> set = $1 /\ $2;
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 f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is finite by SPPOL_1:45;
A2: { (LSeg g,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } is finite by SPPOL_1:45;
A3: { 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(A1, A2);
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 ) } ;
{ 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 ) } ) } = 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

thus { 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 ) } :: according to XBOOLE_0:def 10 :: 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 ) } 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 { 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 A4: 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 ) }
consider X, Y being Subset of (TOP-REAL 2) such that
A5: ( 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 ) } ) by A4;
thus 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 A5, SETFAM_1:def 5; :: thesis: verum

end;

thus 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 ) } ) } :: thesis: verum

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
A6: ( 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 ) } & a = X /\ Y ) by SETFAM_1:def 5;
consider i being Element of NAT such that
A7: ( X = LSeg f,i & 1 <= i & i + 1 <= len f ) by A6;
consider j being Element of NAT such that
A8: ( Y = LSeg g,j & 1 <= j & j + 1 <= len g ) by A6;
reconsider X = X, Y = Y as Subset of (TOP-REAL 2) by A7, A8;
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 A6;
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 A6; :: thesis: verum

end;

end;

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