let 1L be upper-bounded Lattice; :: thesis: for F being ClosedSubset of 1L st Top 1L in F holds

for B being Element of Fin the carrier of 1L st B c= F holds

FinMeet B in F

let F be ClosedSubset of 1L; :: thesis: ( Top 1L in F implies for B being Element of Fin the carrier of 1L st B c= F holds

FinMeet B in F )

defpred S_{1}[ Element of Fin the carrier of 1L] means ( $1 c= F implies FinMeet $1 in F );

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

for p being Element of 1L st S_{1}[B1] holds

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

FinMeet B in F

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

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

for B being Element of Fin the carrier of 1L st B c= F holds

FinMeet B in F

let F be ClosedSubset of 1L; :: thesis: ( Top 1L in F implies for B being Element of Fin the carrier of 1L st B c= F holds

FinMeet B in F )

defpred S

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

for p being Element of 1L st S

S

proof

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

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

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

assume A2: ( B1 c= F implies FinMeet B1 in F ) ; :: thesis: S_{1}[B1 \/ {.p.}]

assume A3: B1 \/ {p} c= F ; :: thesis: FinMeet (B1 \/ {.p.}) in F

then {p} c= F by XBOOLE_1:11;

then p in F by ZFMISC_1:31;

then (FinMeet B1) "/\" p in F by A2, A3, LATTICES:def 24, XBOOLE_1:11;

hence FinMeet (B1 \/ {.p.}) in F by Th21; :: thesis: verum

end;S

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

assume A2: ( B1 c= F implies FinMeet B1 in F ) ; :: thesis: S

assume A3: B1 \/ {p} c= F ; :: thesis: FinMeet (B1 \/ {.p.}) in F

then {p} c= F by XBOOLE_1:11;

then p in F by ZFMISC_1:31;

then (FinMeet B1) "/\" p in F by A2, A3, LATTICES:def 24, XBOOLE_1:11;

hence FinMeet (B1 \/ {.p.}) in F by Th21; :: thesis: verum

FinMeet B in F

then A4: S

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