defpred S₁[ set ] means ( $1 <> {} implies ex x being set st
( x in $1 & ( for y being set st y in $1 holds
x c= y ) ) );
let F be set ; :: thesis:
assume that
A1: not F is empty and
A2: F is with_non-empty_elements and
A3: F is c=-linear ; :: thesis:
thus F <> {} by A1; :: according to FINSET_1:def 3 :: thesis:
let G be set ; :: thesis:
assume that
A4: G <> {} and
A5: G c= F and
A6: G is finite ; :: thesis:

A7: now :: thesis:

let x, B be set ; :: thesis:
assume that
A8: x in G and
A9: B c= G and
A10: S₁[B] ; :: thesis:
thus S₁[B \/ {x}] :: thesis:

proof

assume B \/ {x} <> {} ; :: thesis:

per cases ;

suppose A11: B is empty ; :: thesis:

take x9 = x; :: thesis:
thus x9 in B \/ {x} by A11, TARSKI:def 1; :: thesis:
let y be set ; :: thesis:
thus ( y in B \/ {x} implies x9 c= y ) by A11, TARSKI:def 1; :: thesis:

end;

suppose not B is empty ; :: thesis:

then consider z being set such that
A12: z in B and
A13: for y being set st y in B holds
z c= y by A10;
thus ex x9 being set st
( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) ) :: thesis:

proof

z in G by A9, A12;
then A14: x,z are_c=-comparable by A3, A5, A8, ORDINAL1:def 8;

per cases by A14;

suppose A15: x c= z ; :: thesis:

take x9 = x; :: thesis:
x9 in {x} by TARSKI:def 1;
hence x9 in B \/ {x} by XBOOLE_0:def 3; :: thesis:
let y be set ; :: thesis:
assume A16: y in B \/ {x} ; :: thesis:

per cases by A16, XBOOLE_0:def 3;

suppose y in B ; :: thesis:

then z c= y by A13;
hence x9 c= y by A15; :: thesis:

end;

suppose y in {x} ; :: thesis:

hence x9 c= y by TARSKI:def 1; :: thesis:

end;

end;

end;

suppose A17: z c= x ; :: thesis:

take x9 = z; :: thesis:
thus x9 in B \/ {x} by A12, XBOOLE_0:def 3; :: thesis:
let y be set ; :: thesis:
assume A18: y in B \/ {x} ; :: thesis:

per cases by A18, XBOOLE_0:def 3;

suppose y in B ; :: thesis:

hence x9 c= y by A13; :: thesis:

end;

suppose y in {x} ; :: thesis:

hence x9 c= y by A17, TARSKI:def 1; :: thesis:

end;

end;

end;

end;

end;

end;

end;

end;

end;

A19: S₁[ {} ] ;
S₁[G] from FINSET_1:sch 2(A6, A19, A7);
then consider x being set such that
A20: x in G and
A21: for y being set st y in G holds
x c= y by A4;
consider xe being object such that
A22: xe in x by A2, A5, A20, XBOOLE_0:def 1;

now :: thesis:

let y be set ; :: thesis:
assume y in G ; :: thesis:
then x c= y by A21;
hence xe in y by A22; :: thesis:

end;

hence not meet G = {} by A4, SETFAM_1:def 1; :: thesis: