let L be Lattice; :: thesis: for A being non empty set
for x being Element of A
for B being Finite_Subset of A
for f being Function of A,the carrier of L st x in B holds
FinMeet B,f [= f . x
let A be non empty set ; :: thesis: for x being Element of A
for B being Finite_Subset of A
for f being Function of A,the carrier of L st x in B holds
FinMeet B,f [= f . x
let x be Element of A; :: thesis: for B being Finite_Subset of A
for f being Function of A,the carrier of L st x in B holds
FinMeet B,f [= f . x
let B be Finite_Subset of A; :: thesis: for f being Function of A,the carrier of L st x in B holds
FinMeet B,f [= f . x
let f be Function of A,the carrier of L; :: thesis: ( x in B implies FinMeet B,f [= f . x )
assume A1: x in B ; :: thesis: FinMeet B,f [= f . x
reconsider f' = f as Function of A,the carrier of (L .: ) ;
f' . x [= FinJoin B,f' by A1, Th43;
hence FinMeet B,f [= f . x by Th54; :: thesis: verum