let S be TopStruct ; :: thesis: for X being Subset of S st X is closed_under_lines & X is strong holds

X,X are_joinable

let X be Subset of S; :: thesis: ( X is closed_under_lines & X is strong implies X,X are_joinable )

assume A1: ( X is closed_under_lines & X is strong ) ; :: thesis: X,X are_joinable

reconsider f = <*X*> as FinSequence of bool the carrier of S ;

take f ; :: according to PENCIL_2:def 3 :: thesis: ( X = f . 1 & X = 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))) ) )

thus X = f . 1 by FINSEQ_1:40; :: thesis: ( X = 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))) ) )

len f = 1 by FINSEQ_1:40;

hence X = f . (len f) by FINSEQ_1:40; :: thesis: ( ( 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))) ) )

thus for W being Subset of S st W in rng f holds

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

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

assume that

A2: 1 <= i and

A3: i < len f ; :: thesis: 2 c= card ((f . i) /\ (f . (i + 1)))

thus 2 c= card ((f . i) /\ (f . (i + 1))) by A2, A3, FINSEQ_1:40; :: thesis: verum

X,X are_joinable

let X be Subset of S; :: thesis: ( X is closed_under_lines & X is strong implies X,X are_joinable )

assume A1: ( X is closed_under_lines & X is strong ) ; :: thesis: X,X are_joinable

reconsider f = <*X*> as FinSequence of bool the carrier of S ;

take f ; :: according to PENCIL_2:def 3 :: thesis: ( X = f . 1 & X = 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))) ) )

thus X = f . 1 by FINSEQ_1:40; :: thesis: ( X = 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))) ) )

len f = 1 by FINSEQ_1:40;

hence X = f . (len f) by FINSEQ_1:40; :: thesis: ( ( 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))) ) )

thus for W being Subset of S st W in rng f holds

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

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

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f implies 2 c= card ((f . i) /\ (f . (i + 1))) )
let W be Subset of S; :: thesis: ( W in rng f implies ( W is closed_under_lines & W is strong ) )

assume W in rng f ; :: thesis: ( W is closed_under_lines & W is strong )

then W in {X} by FINSEQ_1:38;

hence ( W is closed_under_lines & W is strong ) by A1, TARSKI:def 1; :: thesis: verum

end;assume W in rng f ; :: thesis: ( W is closed_under_lines & W is strong )

then W in {X} by FINSEQ_1:38;

hence ( W is closed_under_lines & W is strong ) by A1, TARSKI:def 1; :: thesis: verum

assume that

A2: 1 <= i and

A3: i < len f ; :: thesis: 2 c= card ((f . i) /\ (f . (i + 1)))

thus 2 c= card ((f . i) /\ (f . (i + 1))) by A2, A3, FINSEQ_1:40; :: thesis: verum