let 0L be lower-bounded Lattice; :: thesis: for A being ClosedSubset of 0L st Bottom 0L in A holds
for B being Element of Fin the carrier of 0L st B c= A holds
FinJoin B in A
let A be ClosedSubset of 0L; :: thesis: ( Bottom 0L in A implies for B being Element of Fin the carrier of 0L st B c= A holds
FinJoin B in A )
defpred S₁[ Element of Fin the carrier of 0L] means ( $1 c= A implies FinJoin $1 in A );
A1: for B1 being Element of Fin the carrier of 0L
for p being Element of 0L st S₁[B1] holds
S₁[B1 \/ {.p.}]

proof

let B1 be Element of Fin the carrier of 0L; :: thesis: for p being Element of 0L st S₁[B1] holds
S₁[B1 \/ {.p.}]
let p be Element of 0L; :: thesis: ( S₁[B1] implies S₁[B1 \/ {.p.}] )
assume A2: ( B1 c= A implies FinJoin B1 in A ) ; :: thesis: S₁[B1 \/ {.p.}]
assume A3: B1 \/ {p} c= A ; :: thesis: FinJoin (B1 \/ {.p.}) in A
then {p} c= A by XBOOLE_1:11;
then p in A by ZFMISC_1:31;
then (FinJoin B1) "\/" p in A by A2, A3, LATTICES:def 25, XBOOLE_1:11;
hence FinJoin (B1 \/ {.p.}) in A by Th14; :: thesis: verum

end;

assume Bottom 0L in A ; :: thesis: for B being Element of Fin the carrier of 0L st B c= A holds
FinJoin B in A
then A4: S₁[ {}. the carrier of 0L] by Lm1;
thus for B being Element of Fin the carrier of 0L holds S₁[B] from SETWISEO:sch 4(A4, A1); :: thesis: verum