let L be Semilattice; :: thesis: ( L is finite implies L is lower-bounded )

defpred S_{1}[ set ] means ex x being Element of L st x is_<=_than c_{1};

A1: S_{1}[ {} ]
_{1}[B] holds

S_{1}[B \/ {x}]

then A8: the carrier of L is finite ;

thus S_{1}[ the carrier of L]
from FINSET_1:sch 2(A8, A1, A2); :: according to YELLOW_0:def 4 :: thesis: verum

defpred S

A1: S

proof

A2:
for x, B being set st x in the carrier of L & B c= the carrier of L & S
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;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

S

proof

assume
L is finite
; :: thesis: L is lower-bounded
let x, B be set ; :: thesis: ( x in the carrier of L & B c= the carrier of L & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

A3: x in the carrier of L and

B c= the carrier of L ; :: thesis: ( not S_{1}[B] or S_{1}[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_{1}[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 )

hence b <= c by A5, A7, XBOOLE_0:def 3; :: thesis: verum

end;assume that

A3: x in the carrier of L and

B c= the carrier of L ; :: thesis: ( not S

reconsider y = x as Element of L by A3;

given a being Element of L such that A4: a is_<=_than B ; :: thesis: S

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;then A6: a <= c by A4;

a "/\" y <= a by YELLOW_0:23;

hence a "/\" y <= c by A6, ORDERS_2:3; :: thesis: verum

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

assume
c in B \/ {x}
; :: thesis: b <= cassume
c in {x}
; :: thesis: b <= c

then c = y by TARSKI:def 1;

hence b <= c by YELLOW_0:23; :: thesis: verum

end;then c = y by TARSKI:def 1;

hence b <= c by YELLOW_0:23; :: thesis: verum

hence b <= c by A5, A7, XBOOLE_0:def 3; :: thesis: verum

then A8: the carrier of L is finite ;

thus S