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 = {}
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 ) ) );
A7: S₁[ {} ] ;

A8: now

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

proof

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

suppose A12: 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 x' = x; :: thesis: ( x' in B \/ {x} & ( for y being set st y in B \/ {x} holds
x' c= y ) )
thus x' in B \/ {x} by A12, TARSKI:def 1; :: thesis: for y being set st y in B \/ {x} holds
x' c= y
let y be set ; :: thesis: ( y in B \/ {x} implies x' c= y )
thus ( y in B \/ {x} implies x' c= y ) by A12, TARSKI:def 1; :: thesis: verum

end;

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

then 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 A11;
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 ) )
thus ex x' being set st
( x' in B \/ {x} & ( for y being set st y in B \/ {x} holds
x' c= y ) ) :: thesis: verum

proof

z in G by A10, A13;
then A15: x,z are_c=-comparable by A3, A5, A9, 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 x' being set st
( x' in B \/ {x} & ( for y being set st y in B \/ {x} holds
x' c= y ) )

take x' = x; :: thesis: ( x' in B \/ {x} & ( for y being set st y in B \/ {x} holds
x' c= y ) )
x' in {x} by TARSKI:def 1;
hence x' in B \/ {x} by XBOOLE_0:def 3; :: thesis: for y being set st y in B \/ {x} holds
x' c= y
let y be set ; :: thesis: ( y in B \/ {x} implies x' c= y )
assume A17: y in B \/ {x} ; :: thesis: x' c= y
thus x' 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: x' c= y

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

end;

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

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

end;

end;

end;

end;

suppose A18: z c= 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 x' = z; :: thesis: ( x' in B \/ {x} & ( for y being set st y in B \/ {x} holds
x' c= y ) )
thus x' in B \/ {x} by A13, XBOOLE_0:def 3; :: thesis: for y being set st y in B \/ {x} holds
x' c= y
let y be set ; :: thesis: ( y in B \/ {x} implies x' c= y )
assume A19: y in B \/ {x} ; :: thesis: x' c= y
thus x' 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: x' c= y

hence x' c= y by A14; :: thesis: verum

end;

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

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

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

S₁[G] from FINSET_1:sch 2(A6, A7, A8);
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;
x <> {} by A2, A5, A20;
then consider xe being set such that
A22: xe in x by 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 A21;
hence xe in y by A22; :: thesis: verum

end;

hence meet G <> {} by A4, SETFAM_1:def 1; :: thesis: verum