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_maximal_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_maximal_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_maximal_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_maximal_wrt B,the InternalRel of R ) ) & B \/ {y} <> {} implies ex y' being Element of R st
( b₃ in b₂ \/ {y'} & b₃ is_maximal_wrt b₂ \/ {y'},the InternalRel of R ) )
assume that
A5: ( y in X & B c= X ) and
A6: ( B <> {} implies ex x being Element of R st
( x in B & x is_maximal_wrt B,the InternalRel of R ) ) ; :: thesis: ( B \/ {y} <> {} implies ex y' being Element of R st
( b₃ in b₂ \/ {y'} & b₃ is_maximal_wrt b₂ \/ {y'},the InternalRel of R ) )
reconsider y' = y as Element of R by A5;
assume B \/ {y} <> {} ; :: thesis: ex y' being Element of R st
( b₃ in b₂ \/ {y'} & b₃ is_maximal_wrt b₂ \/ {y'},the InternalRel of R )

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

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

take y' = y'; :: thesis: ( y' in B \/ {y} & y' is_maximal_wrt B \/ {y},the InternalRel of R )
thus y' in B \/ {y} by A7, TARSKI:def 1; :: thesis: y' is_maximal_wrt B \/ {y},the InternalRel of R
( y' in B \/ {y} & ( for z being set holds
( not z in B \/ {y'} or not z <> y' or not [y',z] in the InternalRel of R ) ) ) by A7, TARSKI:def 1;
hence y' is_maximal_wrt B \/ {y},the InternalRel of R by WAYBEL_4:def 24; :: thesis: verum

end;

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

then consider x being Element of R such that
A8: ( x in B & x is_maximal_wrt B,the InternalRel of R ) by A6;

now

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

suppose A9: [x,y] in the InternalRel of R ; :: thesis: ex y' being Element of R st
( y' in B \/ {y} & y' is_maximal_wrt B \/ {y},the InternalRel of R )

take y' = y'; :: thesis: ( y' in B \/ {y} & y' is_maximal_wrt B \/ {y},the InternalRel of R )
A10: y in {y} by TARSKI:def 1;
hence y' in B \/ {y} by XBOOLE_0:def 3; :: thesis: y' is_maximal_wrt B \/ {y},the InternalRel of R

now

thus y' in B \/ {y} by A10, XBOOLE_0:def 3; :: thesis: for z being set holds
( not z in B \/ {y} or not z <> y or not [y,z] in the InternalRel of R )

now

assume ex z being set st
( z in B \/ {y} & z <> y & [y,z] in the InternalRel of R ) ; :: thesis: contradiction
then consider z being set such that
A11: ( z in B \/ {y} & z <> y & [y,z] in the InternalRel of R ) ;
( x in the carrier of R & y' in the carrier of R & z in the carrier of R ) by A11, ZFMISC_1:106;
then A12: [x,z] in the InternalRel of R by A1, A9, A11, RELAT_2:def 8;

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

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

now

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

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

then x = y' by A2, A9, A11, RELAT_2:def 4;
hence contradiction by A11, A14; :: thesis: verum

end;

suppose z <> x ; :: thesis: contradiction

hence contradiction by A8, A12, A13, WAYBEL_4:def 24; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

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

end;

end;

end;

hence for z being set holds
( not z in B \/ {y} or not z <> y or not [y,z] in the InternalRel of R ) ; :: thesis: verum

end;

hence y' is_maximal_wrt B \/ {y},the InternalRel of R by WAYBEL_4:def 24; :: thesis: verum

end;

suppose A15: [y,x] in the InternalRel of R ; :: thesis: ex x being Element of R st
( x in B \/ {y} & x is_maximal_wrt B \/ {y},the InternalRel of R )

take x = x; :: thesis: ( x in B \/ {y} & x is_maximal_wrt B \/ {y},the InternalRel of R )
thus x in B \/ {y} by A8, XBOOLE_0:def 3; :: thesis: x is_maximal_wrt B \/ {y},the InternalRel of R

now

thus x in B \/ {y} by A8, XBOOLE_0:def 3; :: thesis: for z being set holds
( not z in B \/ {y} or not z <> x or not [x,z] in the InternalRel of R )

now

assume ex z being set st
( z in B \/ {y} & z <> x & [x,z] in the InternalRel of R ) ; :: thesis: contradiction
then consider z being set such that
A16: ( z in B \/ {y} & z <> x & [x,z] in the InternalRel of R ) ;

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

suppose z in B ; :: thesis: contradiction

hence contradiction by A8, A16, WAYBEL_4:def 24; :: thesis: verum

end;

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

then A17: z = y by TARSKI:def 1;
z in the carrier of R by A16, ZFMISC_1:106;
hence contradiction by A2, A15, A16, A17, RELAT_2:def 4; :: thesis: verum

end;

end;

end;

hence for z being set holds
( not z in B \/ {y} or not z <> x or not [x,z] in the InternalRel of R ) ; :: thesis: verum

end;

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

end;

suppose A18: ( 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_maximal_wrt B \/ {y},the InternalRel of R )

take x = x; :: thesis: ( x in B \/ {y} & x is_maximal_wrt B \/ {y},the InternalRel of R )
thus x in B \/ {y} by A8, XBOOLE_0:def 3; :: thesis: x is_maximal_wrt B \/ {y},the InternalRel of R

now

thus x in B \/ {y} by A8, XBOOLE_0:def 3; :: thesis: for z being set holds
( not z in B \/ {y} or not z <> x or not [x,z] in the InternalRel of R )

now

assume ex z being set st
( z in B \/ {y} & z <> x & [x,z] in the InternalRel of R ) ; :: thesis: contradiction
then consider z being set such that
A19: ( z in B \/ {y} & z <> x & [x,z] in the InternalRel of R ) ;

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

suppose z in B ; :: thesis: contradiction

hence contradiction by A8, A19, WAYBEL_4:def 24; :: thesis: verum

end;

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

hence contradiction by A18, A19, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence for z being set holds
( not z in B \/ {y} or not z <> x or not [x,z] in the InternalRel of R ) ; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;

end;

then A20: 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, A20); :: thesis: verum