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 S1[ 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 S1[B1] holds
S1[B1 \/ {.p.}]
proof
let B1 be Element of Fin the carrier of 1L; :: thesis: for p being Element of 1L st S1[B1] holds
S1[B1 \/ {.p.}]

let p be Element of 1L; :: thesis: ( S1[B1] implies S1[B1 \/ {.p.}] )
assume A2: ( B1 c= F implies FinMeet B1 in F ) ; :: thesis: S1[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 ;
hence FinMeet (B1 \/ {.p.}) in F by Th21; :: thesis: verum
end;
assume Top 1L in F ; :: thesis: for B being Element of Fin the carrier of 1L st B c= F holds
FinMeet B in F

then A4: S1[ {}. the carrier of 1L] by Lm2;
thus for B being Element of Fin the carrier of 1L holds S1[B] from :: thesis: verum