defpred S_{1}[ set , set ] means 2 c= card ($1 /\ $2);

let S be TopStruct ; :: thesis: for X, Y being Subset of S st X,Y are_joinable holds

ex f being one-to-one FinSequence of bool the carrier of S st

( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) )

let X, Y be Subset of S; :: thesis: ( X,Y are_joinable implies ex f being one-to-one FinSequence of bool the carrier of S st

( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) ) )

assume X,Y are_joinable ; :: thesis: ex f being one-to-one FinSequence of bool the carrier of S st

( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) )

then consider f being FinSequence of bool the carrier of S such that

A1: ( X = f . 1 & Y = f . (len f) ) and

A2: for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) and

A3: for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ;

A4: for i being Element of NAT

for d1, d2 being set st 1 <= i & i < len f & d1 = f . i & d2 = f . (i + 1) holds

S_{1}[d1,d2]
by A3;

consider g being one-to-one FinSequence of bool the carrier of S such that

A5: ( X = g . 1 & Y = g . (len g) ) and

A6: rng g c= rng f and

A7: for i being Element of NAT st 1 <= i & i < len g holds

S_{1}[g . i,g . (i + 1)]
from PENCIL_2:sch 1(A1, A4);

take g ; :: thesis: ( X = g . 1 & Y = g . (len g) & ( for W being Subset of S st W in rng g holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len g holds

2 c= card ((g . i) /\ (g . (i + 1))) ) )

thus ( X = g . 1 & Y = g . (len g) & ( for W being Subset of S st W in rng g holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len g holds

2 c= card ((g . i) /\ (g . (i + 1))) ) ) by A2, A5, A6, A7; :: thesis: verum

let S be TopStruct ; :: thesis: for X, Y being Subset of S st X,Y are_joinable holds

ex f being one-to-one FinSequence of bool the carrier of S st

( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) )

let X, Y be Subset of S; :: thesis: ( X,Y are_joinable implies ex f being one-to-one FinSequence of bool the carrier of S st

( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) ) )

assume X,Y are_joinable ; :: thesis: ex f being one-to-one FinSequence of bool the carrier of S st

( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) )

then consider f being FinSequence of bool the carrier of S such that

A1: ( X = f . 1 & Y = f . (len f) ) and

A2: for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) and

A3: for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ;

A4: for i being Element of NAT

for d1, d2 being set st 1 <= i & i < len f & d1 = f . i & d2 = f . (i + 1) holds

S

consider g being one-to-one FinSequence of bool the carrier of S such that

A5: ( X = g . 1 & Y = g . (len g) ) and

A6: rng g c= rng f and

A7: for i being Element of NAT st 1 <= i & i < len g holds

S

take g ; :: thesis: ( X = g . 1 & Y = g . (len g) & ( for W being Subset of S st W in rng g holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len g holds

2 c= card ((g . i) /\ (g . (i + 1))) ) )

thus ( X = g . 1 & Y = g . (len g) & ( for W being Subset of S st W in rng g holds

( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len g holds

2 c= card ((g . i) /\ (g . (i + 1))) ) ) by A2, A5, A6, A7; :: thesis: verum