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

y <= x ) )

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

y <= x ) ) )

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

y <= x ) )

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

y <= x ) ) );

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

y <= x ) ) 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

y <= x ) )

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

y <= x ) ) )

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

y <= x ) )

defpred S

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

y <= x ) ) );

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

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

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

y <= x ) )

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

y <= x ) ) ) 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

y <= x ) ) ) 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

y <= x ) )

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

y <= x ) )

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

y <= z ) )

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

y <= z

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

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

hence y <= z 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

y <= z ) )

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

y <= z

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

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

hence y <= z 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

y <= x ) )

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

y <= x ) )

A13:
not A is empty
by A5;

reconsider z = z as Element of A by A5;

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

z <> x by A12, A8, A10;

end;reconsider z = z as Element of A by A5;

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

z <> x by A12, A8, A10;

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

end;

suppose A15:
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

y <= x ) )

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

y <= x ) )

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

y <= z ) )

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

y <= z

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

assume that

A16: y in C \/ {z} and

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

end;y <= z ) )

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

y <= z

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

assume that

A16: y in C \/ {z} and

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

suppose A19:
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

y <= x ) )

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

y <= x ) )

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

y <= x ) )

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

y <= x

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

assume that

A20: y in C \/ {z} and

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

end;y <= x ) )

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

y <= x

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

assume that

A20: y in C \/ {z} and

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

hence ex x being Element of A st

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

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