let R be non empty transitive antisymmetric RelStr ; :: thesis: for X being finite Subset of R st X <> {} holds

ex x being Element of R st

( x in X & x is_minimal_wrt X, the InternalRel of R )

let X be finite Subset of R; :: thesis: ( X <> {} implies ex x being Element of R st

( x in X & x is_minimal_wrt X, the InternalRel of R ) )

set IR = the InternalRel of R;

set CR = the carrier of R;

A1: the InternalRel of R is_transitive_in the carrier of R by ORDERS_2:def 3;

A2: the InternalRel of R is_antisymmetric_in the carrier of R by ORDERS_2:def 4;

A3: X is finite ;

defpred S_{1}[ set ] means ( $1 <> {} implies ex x being Element of R st

( x in $1 & x is_minimal_wrt $1, the InternalRel of R ) );

A4: S_{1}[ {} ]
;

_{1}[B] holds

S_{1}[B \/ {y}]
;

thus S_{1}[X]
from FINSET_1:sch 2(A3, A4, A32); :: thesis: verum

ex x being Element of R st

( x in X & x is_minimal_wrt X, the InternalRel of R )

let X be finite Subset of R; :: thesis: ( X <> {} implies ex x being Element of R st

( x in X & x is_minimal_wrt X, the InternalRel of R ) )

set IR = the InternalRel of R;

set CR = the carrier of R;

A1: the InternalRel of R is_transitive_in the carrier of R by ORDERS_2:def 3;

A2: the InternalRel of R is_antisymmetric_in the carrier of R by ORDERS_2:def 4;

A3: X is finite ;

defpred S

( x in $1 & x is_minimal_wrt $1, the InternalRel of R ) );

A4: S

now :: thesis: for y, B being set st y in X & B c= X & ( B <> {} implies ex x being Element of R st

( x in B & x is_minimal_wrt B, the InternalRel of R ) ) & B \/ {y} <> {} holds

ex y9 being Element of R st

( y9 in B \/ {y} & y9 is_minimal_wrt B \/ {y}, the InternalRel of R )

then A32:
for y, B being set st y in X & B c= X & S( x in B & x is_minimal_wrt B, the InternalRel of R ) ) & B \/ {y} <> {} holds

ex y9 being Element of R st

( y9 in B \/ {y} & y9 is_minimal_wrt B \/ {y}, the InternalRel of R )

let y, B be set ; :: thesis: ( y in X & B c= X & ( B <> {} implies ex x being Element of R st

( x in B & x is_minimal_wrt B, the InternalRel of R ) ) & B \/ {y} <> {} implies ex y9 being Element of R st

( b_{3} in b_{2} \/ {y9} & b_{3} is_minimal_wrt b_{2} \/ {y9}, the InternalRel of R ) )

assume that

A5: y in X and

B c= X and

A6: ( B <> {} implies ex x being Element of R st

( x in B & x is_minimal_wrt B, the InternalRel of R ) ) ; :: thesis: ( B \/ {y} <> {} implies ex y9 being Element of R st

( b_{3} in b_{2} \/ {y9} & b_{3} is_minimal_wrt b_{2} \/ {y9}, the InternalRel of R ) )

reconsider y9 = y as Element of R by A5;

assume B \/ {y} <> {} ; :: thesis: ex y9 being Element of R st

( b_{3} in b_{2} \/ {y9} & b_{3} is_minimal_wrt b_{2} \/ {y9}, the InternalRel of R )

end;( x in B & x is_minimal_wrt B, the InternalRel of R ) ) & B \/ {y} <> {} implies ex y9 being Element of R st

( b

assume that

A5: y in X and

B c= X and

A6: ( B <> {} implies ex x being Element of R st

( x in B & x is_minimal_wrt B, the InternalRel of R ) ) ; :: thesis: ( B \/ {y} <> {} implies ex y9 being Element of R st

( b

reconsider y9 = y as Element of R by A5;

assume B \/ {y} <> {} ; :: thesis: ex y9 being Element of R st

( b

per cases
( B = {} or B <> {} )
;

end;

suppose A7:
B = {}
; :: thesis: ex y9 being Element of R st

( b_{3} in b_{2} \/ {y9} & b_{3} is_minimal_wrt b_{2} \/ {y9}, the InternalRel of R )

( b

take y9 = y9; :: thesis: ( y9 in B \/ {y} & y9 is_minimal_wrt B \/ {y}, the InternalRel of R )

thus y9 in B \/ {y} by A7, TARSKI:def 1; :: thesis: y9 is_minimal_wrt B \/ {y}, the InternalRel of R

A8: y9 in B \/ {y} by A7, TARSKI:def 1;

for z being set holds

( not z in B \/ {y9} or not z <> y9 or not [z,y9] in the InternalRel of R ) by A7, TARSKI:def 1;

hence y9 is_minimal_wrt B \/ {y}, the InternalRel of R by A8, WAYBEL_4:def 25; :: thesis: verum

end;thus y9 in B \/ {y} by A7, TARSKI:def 1; :: thesis: y9 is_minimal_wrt B \/ {y}, the InternalRel of R

A8: y9 in B \/ {y} by A7, TARSKI:def 1;

for z being set holds

( not z in B \/ {y9} or not z <> y9 or not [z,y9] in the InternalRel of R ) by A7, TARSKI:def 1;

hence y9 is_minimal_wrt B \/ {y}, the InternalRel of R by A8, WAYBEL_4:def 25; :: thesis: verum

suppose
B <> {}
; :: thesis: ex x being Element of R st

( b_{3} in b_{2} \/ {x} & b_{3} is_minimal_wrt b_{2} \/ {x}, the InternalRel of R )

( b

then consider x being Element of R such that

A9: x in B and

A10: x is_minimal_wrt B, the InternalRel of R by A6;

( x in B \/ {y} & x is_minimal_wrt B \/ {y}, the InternalRel of R ) ; :: thesis: verum

end;A9: x in B and

A10: x is_minimal_wrt B, the InternalRel of R by A6;

now :: thesis: ex y9 being Element of R st

( y9 in B \/ {y} & y9 is_minimal_wrt B \/ {y}, the InternalRel of R )end;

hence
ex x being Element of R st ( y9 in B \/ {y} & y9 is_minimal_wrt B \/ {y}, the InternalRel of R )

per cases
( [y,x] in the InternalRel of R or [x,y] in the InternalRel of R or ( not [x,y] in the InternalRel of R & not [y,x] in the InternalRel of R ) )
;

end;

suppose A11:
[y,x] in the InternalRel of R
; :: thesis: ex y9 being Element of R st

( y9 in B \/ {y} & y9 is_minimal_wrt B \/ {y}, the InternalRel of R )

( y9 in B \/ {y} & y9 is_minimal_wrt B \/ {y}, the InternalRel of R )

take y9 = y9; :: thesis: ( y9 in B \/ {y} & y9 is_minimal_wrt B \/ {y}, the InternalRel of R )

A12: y in {y} by TARSKI:def 1;

hence y9 in B \/ {y} by XBOOLE_0:def 3; :: thesis: y9 is_minimal_wrt B \/ {y}, the InternalRel of R

hence y9 is_minimal_wrt B \/ {y}, the InternalRel of R by A13, WAYBEL_4:def 25; :: thesis: verum

end;A12: y in {y} by TARSKI:def 1;

hence y9 in B \/ {y} by XBOOLE_0:def 3; :: thesis: y9 is_minimal_wrt B \/ {y}, the InternalRel of R

A13: now :: thesis: for z being set holds

( not z in B \/ {y} or not z <> y or not [z,y] in the InternalRel of R )

y9 in B \/ {y}
by A12, XBOOLE_0:def 3;( not z in B \/ {y} or not z <> y or not [z,y] in the InternalRel of R )

assume
ex z being set st

( z in B \/ {y} & z <> y & [z,y] in the InternalRel of R ) ; :: thesis: contradiction

then consider z being set such that

A14: z in B \/ {y} and

A15: z <> y and

A16: [z,y] in the InternalRel of R ;

A17: y9 in the carrier of R ;

z in the carrier of R by A16, ZFMISC_1:87;

then A18: [z,x] in the InternalRel of R by A1, A11, A16, A17;

end;( z in B \/ {y} & z <> y & [z,y] in the InternalRel of R ) ; :: thesis: contradiction

then consider z being set such that

A14: z in B \/ {y} and

A15: z <> y and

A16: [z,y] in the InternalRel of R ;

A17: y9 in the carrier of R ;

z in the carrier of R by A16, ZFMISC_1:87;

then A18: [z,x] in the InternalRel of R by A1, A11, A16, A17;

per cases
( z in B or z in {y} )
by A14, XBOOLE_0:def 3;

end;

suppose A19:
z in B
; :: thesis: contradiction

end;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;

hence y9 is_minimal_wrt B \/ {y}, the InternalRel of R by A13, WAYBEL_4:def 25; :: thesis: verum

suppose A21:
[x,y] in the InternalRel of R
; :: thesis: ex x being Element of R st

( x in B \/ {y} & x is_minimal_wrt B \/ {y}, the InternalRel of R )

( x in B \/ {y} & x is_minimal_wrt B \/ {y}, the InternalRel of R )

take x = x; :: thesis: ( x in B \/ {y} & x is_minimal_wrt B \/ {y}, the InternalRel of R )

thus x in B \/ {y} by A9, XBOOLE_0:def 3; :: thesis: x is_minimal_wrt B \/ {y}, the InternalRel of R

hence x is_minimal_wrt B \/ {y}, the InternalRel of R by A22, WAYBEL_4:def 25; :: thesis: verum

end;thus x in B \/ {y} by A9, XBOOLE_0:def 3; :: thesis: x is_minimal_wrt B \/ {y}, the InternalRel of R

A22: now :: thesis: for z being set holds

( not z in B \/ {y} or not z <> x or not [z,x] in the InternalRel of R )

x in B \/ {y}
by A9, XBOOLE_0:def 3;( not z in B \/ {y} or not z <> x or not [z,x] in the InternalRel of R )

assume
ex z being set st

( z in B \/ {y} & z <> x & [z,x] in the InternalRel of R ) ; :: thesis: contradiction

then consider z being set such that

A23: z in B \/ {y} and

A24: z <> x and

A25: [z,x] in the InternalRel of R ;

end;( z in B \/ {y} & z <> x & [z,x] in the InternalRel of R ) ; :: thesis: contradiction

then consider z being set such that

A23: z in B \/ {y} and

A24: z <> x and

A25: [z,x] in the InternalRel of R ;

per cases
( z in B or z in {y} )
by A23, XBOOLE_0:def 3;

end;

suppose
z in {y}
; :: thesis: contradiction

then A26:
z = y
by TARSKI:def 1;

z in the carrier of R by A25, ZFMISC_1:87;

hence contradiction by A2, A21, A24, A25, A26; :: thesis: verum

end;z in the carrier of R by A25, ZFMISC_1:87;

hence contradiction by A2, A21, A24, A25, A26; :: thesis: verum

hence x is_minimal_wrt B \/ {y}, the InternalRel of R by A22, WAYBEL_4:def 25; :: thesis: verum

suppose A27:
( not [x,y] in the InternalRel of R & not [y,x] in the InternalRel of R )
; :: thesis: ex x being Element of R st

( x in B \/ {y} & x is_minimal_wrt B \/ {y}, the InternalRel of R )

( x in B \/ {y} & x is_minimal_wrt B \/ {y}, the InternalRel of R )

take x = x; :: thesis: ( x in B \/ {y} & x is_minimal_wrt B \/ {y}, the InternalRel of R )

thus x in B \/ {y} by A9, XBOOLE_0:def 3; :: thesis: x is_minimal_wrt B \/ {y}, the InternalRel of R

hence x is_minimal_wrt B \/ {y}, the InternalRel of R by A28, WAYBEL_4:def 25; :: thesis: verum

end;thus x in B \/ {y} by A9, XBOOLE_0:def 3; :: thesis: x is_minimal_wrt B \/ {y}, the InternalRel of R

A28: now :: thesis: for z being set holds

( not z in B \/ {y} or not z <> x or not [z,x] in the InternalRel of R )

x in B \/ {y}
by A9, XBOOLE_0:def 3;( not z in B \/ {y} or not z <> x or not [z,x] in the InternalRel of R )

assume
ex z being set st

( z in B \/ {y} & z <> x & [z,x] in the InternalRel of R ) ; :: thesis: contradiction

then consider z being set such that

A29: z in B \/ {y} and

A30: z <> x and

A31: [z,x] in the InternalRel of R ;

end;( z in B \/ {y} & z <> x & [z,x] in the InternalRel of R ) ; :: thesis: contradiction

then consider z being set such that

A29: z in B \/ {y} and

A30: z <> x and

A31: [z,x] in the InternalRel of R ;

hence x is_minimal_wrt B \/ {y}, the InternalRel of R by A28, WAYBEL_4:def 25; :: thesis: verum

( x in B \/ {y} & x is_minimal_wrt B \/ {y}, the InternalRel of R ) ; :: thesis: verum

S

thus S