let L be Semilattice; :: thesis: ( L is finite implies L is lower-bounded )
defpred S₁[ set ] means ex x being Element of L st x is_<=_than c₁;
A1: S₁[ {} ]

proof

set a = the Element of L;
take the Element of L ; :: thesis: the Element of L is_<=_than {}
let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in {} or the Element of L <= b )
assume b in {} ; :: thesis: the Element of L <= b
hence the Element of L <= b ; :: thesis: verum

end;

A2: for x, B being set st x in the carrier of L & B c= the carrier of L & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in the carrier of L & B c= the carrier of L & S₁[B] implies S₁[B \/ {x}] )
assume that
A3: x in the carrier of L and
B c= the carrier of L ; :: thesis: ( not S₁[B] or S₁[B \/ {x}] )
reconsider y = x as Element of L by A3;
given a being Element of L such that A4: a is_<=_than B ; :: thesis: S₁[B \/ {x}]
take b = a "/\" y; :: thesis: b is_<=_than B \/ {x}
let c be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not c in B \/ {x} or b <= c )

A5: now :: thesis: ( c in B implies a "/\" y <= c )

assume c in B ; :: thesis: a "/\" y <= c
then A6: a <= c by A4;
a "/\" y <= a by YELLOW_0:23;
hence a "/\" y <= c by A6, ORDERS_2:3; :: thesis: verum

end;

A7: now :: thesis: ( c in {x} implies b <= c )

assume c in {x} ; :: thesis: b <= c
then c = y by TARSKI:def 1;
hence b <= c by YELLOW_0:23; :: thesis: verum

end;

assume c in B \/ {x} ; :: thesis: b <= c
hence b <= c by A5, A7, XBOOLE_0:def 3; :: thesis: verum

end;

assume L is finite ; :: thesis: L is lower-bounded
then A8: the carrier of L is finite ;
thus S₁[ the carrier of L] from FINSET_1:sch 2(A8, A1, A2); :: according to YELLOW_0:def 4 :: thesis: verum