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_{1}[ 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_{1}[B1] holds

S_{1}[B1 \/ {.p.}]

FinJoin B in A

then A4: S_{1}[ {}. the carrier of 0L]
by Lm1;

thus for B being Element of Fin the carrier of 0L holds S_{1}[B]
from SETWISEO:sch 4(A4, A1); :: thesis: verum

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

A1: for B1 being Element of Fin the carrier of 0L

for p being Element of 0L st S

S

proof

assume
Bottom 0L in A
; :: thesis: for B being Element of Fin the carrier of 0L st B c= A holds
let B1 be Element of Fin the carrier of 0L; :: thesis: for p being Element of 0L st S_{1}[B1] holds

S_{1}[B1 \/ {.p.}]

let p be Element of 0L; :: thesis: ( S_{1}[B1] implies S_{1}[B1 \/ {.p.}] )

assume A2: ( B1 c= A implies FinJoin B1 in A ) ; :: thesis: S_{1}[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;S

let p be Element of 0L; :: thesis: ( S

assume A2: ( B1 c= A implies FinJoin B1 in A ) ; :: thesis: S

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

FinJoin B in A

then A4: S

thus for B being Element of Fin the carrier of 0L holds S