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₁[ 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₁[B1] holds
S₁[B1 \/ {.p.}]

proof

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

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: S₁[ {}. the carrier of 1L] by Lm2;
thus for B being Element of Fin the carrier of 1L holds S₁[B] from SETWISEO:sch 4(A4, A1); :: thesis: verum