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: ( not F is empty & F is without_zero & F is c=-linear implies F is centered )
assume that
A1: not F is empty and
A2: F is without_zero and
A3: F is c=-linear ; :: thesis: F is centered
thus F <> {} by A1; :: according to FINSET_1:def 3 :: thesis: for b₁ being set holds
( b₁ = {} or not b₁ c= F or not b₁ is finite or not meet b₁ = {} )
let G be set ; :: thesis: ( G = {} or not G c= F or not G is finite or not meet G = {} )
assume that
A4: G <> {} and
A5: G c= F and
A6: G is finite ; :: thesis: not meet G = {}

A7: now

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

proof

per cases ( B is empty or not B is empty ) ;

suppose A11: B is empty ; :: thesis: S₁[B \/ {x}]

assume B \/ {x} <> {} ; :: thesis: ex x being set st
( x in B \/ {x} & ( for y being set st y in B \/ {x} holds
x c= y ) )
take x9 = x; :: thesis: ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )
thus x9 in B \/ {x} by A11, TARSKI:def 1; :: thesis: for y being set st y in B \/ {x} holds
x9 c= y
let y be set ; :: thesis: ( y in B \/ {x} implies x9 c= y )
thus ( y in B \/ {x} implies x9 c= y ) by A11, TARSKI:def 1; :: thesis: verum

end;

suppose A12: not B is empty ; :: thesis: S₁[B \/ {x}]

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

proof

z in G by A9, A13;
then A15: x,z are_c=-comparable by A3, A5, A8, ORDINAL1:def 9;

per cases ( x c= z or z c= x ) by A15, XBOOLE_0:def 9;

suppose A16: x c= z ; :: thesis: ex x9 being set st
( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )

take x9 = x; :: thesis: ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )
x9 in {x} by TARSKI:def 1;
hence x9 in B \/ {x} by XBOOLE_0:def 3; :: thesis: for y being set st y in B \/ {x} holds
x9 c= y
let y be set ; :: thesis: ( y in B \/ {x} implies x9 c= y )
assume A17: y in B \/ {x} ; :: thesis: x9 c= y
thus x9 c= y :: thesis: verum

proof

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

suppose y in B ; :: thesis: x9 c= y

then z c= y by A14;
hence x9 c= y by A16, XBOOLE_1:1; :: thesis: verum

end;

suppose y in {x} ; :: thesis: x9 c= y

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

end;

end;

end;

end;

suppose A18: z c= x ; :: thesis: ex x9 being set st
( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )

take x9 = z; :: thesis: ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )
thus x9 in B \/ {x} by A13, XBOOLE_0:def 3; :: thesis: for y being set st y in B \/ {x} holds
x9 c= y
let y be set ; :: thesis: ( y in B \/ {x} implies x9 c= y )
assume A19: y in B \/ {x} ; :: thesis: x9 c= y
thus x9 c= y :: thesis: verum

proof

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

suppose y in B ; :: thesis: x9 c= y

hence x9 c= y by A14; :: thesis: verum

end;

suppose y in {x} ; :: thesis: x9 c= y

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

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

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

now

let y be set ; :: thesis: ( y in G implies xe in y )
assume y in G ; :: thesis: xe in y
then x c= y by A22;
hence xe in y by A23; :: thesis: verum

end;

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