let L be Semilattice; :: thesis: ( L is finite implies L is lower-bounded )
defpred S1[ set ] means ex x being Element of L st x is_<=_than c1;
A1: S1[ {} ]
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 & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in the carrier of L & B c= the carrier of L & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in the carrier of L and
B c= the carrier of L ; :: thesis: ( not S1[B] or S1[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: S1[B \/ {x}]
take b = a "/\" y; :: thesis:
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 ; :: thesis: verum
end;
A7: now :: thesis: ( c in {x} implies b <= c )end;
assume c in B \/ {x} ; :: thesis: b <= c
hence b <= c by ; :: thesis: verum
end;
assume L is finite ; :: thesis:
then A8: the carrier of L is finite ;
thus S1[ the carrier of L] from FINSET_1:sch 2(A8, A1, A2); :: according to YELLOW_0:def 4 :: thesis: verum