let L be Lattice; :: thesis: for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet B,f [= u
let u be Element of L; :: thesis: for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet B,f [= u
let A be non empty set ; :: thesis: for B being Finite_Subset of A
for f being Function of A,the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet B,f [= u
let B be Finite_Subset of A; :: thesis: for f being Function of A,the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet B,f [= u
let f be Function of A,the carrier of L; :: thesis: ( ex x being Element of A st
( x in B & f . x [= u ) implies FinMeet B,f [= u )
given x being Element of A such that A1: x in B and
A2: f . x [= u ; :: thesis: FinMeet B,f [= u
reconsider f' = f as Function of A,the carrier of (L .: ) ;
reconsider u' = u as Element of (L .: ) ;
u' [= f' . x by A2, Th53;
then u' [= FinJoin B,f' by A1, Th44;
hence FinMeet B,f [= u by Th54; :: thesis: verum