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 5;
A2: the InternalRel of R is_antisymmetric_in the carrier of R by ORDERS_2:def 6;
A3: X is finite ;
defpred S₁[ 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₁[ {} ] ;

now

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₃ in b₂ \/ {y9} & b₃ is_minimal_wrt b₂ \/ {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₃ in b₂ \/ {y9} & b₃ is_minimal_wrt b₂ \/ {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₃ in b₂ \/ {y9} & b₃ is_minimal_wrt b₂ \/ {y9},the InternalRel of R )

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

suppose A7: B = {} ; :: thesis: ex y9 being Element of R st
( b₃ in b₂ \/ {y9} & b₃ is_minimal_wrt b₂ \/ {y9},the InternalRel of R )

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 26; :: thesis: verum

end;

suppose B <> {} ; :: thesis: ex x being Element of R st
( b₃ in b₂ \/ {x} & b₃ is_minimal_wrt b₂ \/ {x},the InternalRel of R )

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;

now

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 ) ) ;

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 )

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

A13: now

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:106;
then A18: [z,x] in the InternalRel of R by A1, A11, A16, A17, RELAT_2:def 8;

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

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

now

per cases ( z = x or z <> x ) ;

suppose A20: z = x ; :: thesis: contradiction

then x = y9 by A2, A11, A16, RELAT_2:def 4;
hence contradiction by A15, A20; :: thesis: verum

end;

suppose z <> x ; :: thesis: contradiction

hence contradiction by A10, A18, A19, WAYBEL_4:def 26; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

hence contradiction by A15, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

end;

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 )

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

A22: now

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 ;

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

suppose z in B ; :: thesis: contradiction

hence contradiction by A10, A24, A25, WAYBEL_4:def 26; :: thesis: verum

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:106;
hence contradiction by A2, A21, A24, A25, A26, RELAT_2:def 4; :: thesis: verum

end;

end;

end;

x in B \/ {y} by A9, XBOOLE_0:def 3;
hence x is_minimal_wrt B \/ {y},the InternalRel of R by A22, WAYBEL_4:def 26; :: thesis: verum

end;

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 )

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

A28: now

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 ;

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

suppose z in B ; :: thesis: contradiction

hence contradiction by A10, A30, A31, WAYBEL_4:def 26; :: thesis: verum

end;

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

hence contradiction by A27, A31, TARSKI:def 1; :: thesis: verum

end;

end;

end;

x in B \/ {y} by A9, XBOOLE_0:def 3;
hence x is_minimal_wrt B \/ {y},the InternalRel of R by A28, WAYBEL_4:def 26; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

then A32: for y, B being set st y in X & B c= X & S₁[B] holds
S₁[B \/ {y}] ;
thus S₁[X] from FINSET_1:sch 2(A3, A4, A32); :: thesis: verum