defpred S₁[ 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₁[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₁[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