let A be transitive RelStr ; :: thesis: for B being finite Subset of A st not B is empty & the InternalRel of A is_connected_in B holds

ex x being Element of A st

( x in B & ( for y being Element of A st y in B & x <> y holds

x <= y ) )

let B be finite Subset of A; :: thesis: ( not B is empty & the InternalRel of A is_connected_in B implies ex x being Element of A st

( x in B & ( for y being Element of A st y in B & x <> y holds

x <= y ) ) )

assume A1: ( not B is empty & the InternalRel of A is_connected_in B ) ; :: thesis: ex x being Element of A st

( x in B & ( for y being Element of A st y in B & x <> y holds

x <= y ) )

defpred S_{1}[ set ] means ( not $1 is empty implies ex x being Element of A st

( x in $1 & ( for y being Element of A st y in $1 & x <> y holds

x <= y ) ) );

A2: B is finite ;

A3: S_{1}[ {} ]
;

A4: for z, C being set st z in B & C c= B & S_{1}[C] holds

S_{1}[C \/ {z}]
_{1}[B]
from FINSET_1:sch 2(A2, A3, A4);

hence ex x being Element of A st

( x in B & ( for y being Element of A st y in B & x <> y holds

x <= y ) ) by A1; :: thesis: verum

ex x being Element of A st

( x in B & ( for y being Element of A st y in B & x <> y holds

x <= y ) )

let B be finite Subset of A; :: thesis: ( not B is empty & the InternalRel of A is_connected_in B implies ex x being Element of A st

( x in B & ( for y being Element of A st y in B & x <> y holds

x <= y ) ) )

assume A1: ( not B is empty & the InternalRel of A is_connected_in B ) ; :: thesis: ex x being Element of A st

( x in B & ( for y being Element of A st y in B & x <> y holds

x <= y ) )

defpred S

( x in $1 & ( for y being Element of A st y in $1 & x <> y holds

x <= y ) ) );

A2: B is finite ;

A3: S

A4: for z, C being set st z in B & C c= B & S

S

proof

S
let z, C be set ; :: thesis: ( z in B & C c= B & S_{1}[C] implies S_{1}[C \/ {z}] )

assume that

A5: z in B and

A6: C c= B and

A7: S_{1}[C]
; :: thesis: S_{1}[C \/ {z}]

set D = C \/ {z};

end;assume that

A5: z in B and

A6: C c= B and

A7: S

set D = C \/ {z};

per cases
( z in C or not z in C )
;

end;

suppose A8:
not z in C
; :: thesis: S_{1}[C \/ {z}]

ex x being Element of A st

( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )_{1}[C \/ {z}]
; :: thesis: verum

end;( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

proof

hence
S
z in {z}
by TARSKI:def 1;

then A9: z in C \/ {z} by XBOOLE_0:def 3;

consider x being Element of A such that

A10: ( not C is empty implies ( x in C & ( for y being Element of A st y in C & x <> y holds

x <= y ) ) ) by A7;

end;then A9: z in C \/ {z} by XBOOLE_0:def 3;

consider x being Element of A such that

A10: ( not C is empty implies ( x in C & ( for y being Element of A st y in C & x <> y holds

x <= y ) ) ) by A7;

per cases
( C is empty or not C is empty )
;

end;

suppose A11:
C is empty
; :: thesis: ex x being Element of A st

( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

reconsider z = z as Element of A by A5;

take z ; :: thesis: ( z in C \/ {z} & ( for y being Element of A st y in C \/ {z} & z <> y holds

z <= y ) )

thus z in C \/ {z} by A9; :: thesis: for y being Element of A st y in C \/ {z} & z <> y holds

z <= y

let y be Element of A; :: thesis: ( y in C \/ {z} & z <> y implies z <= y )

assume ( y in C \/ {z} & z <> y ) ; :: thesis: z <= y

hence z <= y by A11, TARSKI:def 1; :: thesis: verum

end;take z ; :: thesis: ( z in C \/ {z} & ( for y being Element of A st y in C \/ {z} & z <> y holds

z <= y ) )

thus z in C \/ {z} by A9; :: thesis: for y being Element of A st y in C \/ {z} & z <> y holds

z <= y

let y be Element of A; :: thesis: ( y in C \/ {z} & z <> y implies z <= y )

assume ( y in C \/ {z} & z <> y ) ; :: thesis: z <= y

hence z <= y by A11, TARSKI:def 1; :: thesis: verum

suppose A12:
not C is empty
; :: thesis: ex x being Element of A st

( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

A13:
not A is empty
by A5;

A14: x in B by A12, A10, A6;

reconsider z = z as Element of A by A5;

z <> x by A12, A8, A10;

end;A14: x in B by A12, A10, A6;

reconsider z = z as Element of A by A5;

z <> x by A12, A8, A10;

per cases then
( z <= x or x <= z )
by A1, A13, A5, A14, Th26;

end;

suppose A15:
z <= x
; :: thesis: ex x being Element of A st

( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

take
z
; :: thesis: ( z in C \/ {z} & ( for y being Element of A st y in C \/ {z} & z <> y holds

z <= y ) )

thus z in C \/ {z} by A9; :: thesis: for y being Element of A st y in C \/ {z} & z <> y holds

z <= y

let y be Element of A; :: thesis: ( y in C \/ {z} & z <> y implies z <= y )

assume that

A16: y in C \/ {z} and

A17: z <> y ; :: thesis: z <= y

end;z <= y ) )

thus z in C \/ {z} by A9; :: thesis: for y being Element of A st y in C \/ {z} & z <> y holds

z <= y

let y be Element of A; :: thesis: ( y in C \/ {z} & z <> y implies z <= y )

assume that

A16: y in C \/ {z} and

A17: z <> y ; :: thesis: z <= y

suppose A19:
x <= z
; :: thesis: ex x being Element of A st

( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

take
x
; :: thesis: ( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds

x <= y ) )

thus x in C \/ {z} by A12, A10, XBOOLE_0:def 3; :: thesis: for y being Element of A st y in C \/ {z} & x <> y holds

x <= y

let y be Element of A; :: thesis: ( y in C \/ {z} & x <> y implies x <= y )

assume that

A20: y in C \/ {z} and

A21: x <> y ; :: thesis: x <= y

end;x <= y ) )

thus x in C \/ {z} by A12, A10, XBOOLE_0:def 3; :: thesis: for y being Element of A st y in C \/ {z} & x <> y holds

x <= y

let y be Element of A; :: thesis: ( y in C \/ {z} & x <> y implies x <= y )

assume that

A20: y in C \/ {z} and

A21: x <> y ; :: thesis: x <= y

hence ex x being Element of A st

( x in B & ( for y being Element of A st y in B & x <> y holds

x <= y ) ) by A1; :: thesis: verum