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 ( for x being Element of A st x in B holds
f . x = u ) & B <> {} 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 ( for x being Element of A st x in B holds
f . x = u ) & B <> {} 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 ( for x being Element of A st x in B holds
f . x = u ) & B <> {} holds
FinMeet B,f = u
let B be Finite_Subset of A; :: thesis: for f being Function of A,the carrier of L st ( for x being Element of A st x in B holds
f . x = u ) & B <> {} holds
FinMeet B,f = u
let f be Function of A,the carrier of L; :: thesis: ( ( for x being Element of A st x in B holds
f . x = u ) & B <> {} implies FinMeet B,f = u )
reconsider f9 = f as Function of A,the carrier of (L .: ) ;
A1: FinJoin B,f9 = FinMeet B,f ;
assume ( ( for x being Element of A st x in B holds
f . x = u ) & B <> {} ) ; :: thesis: FinMeet B,f = u
hence FinMeet B,f = u by A1, SETWISEO:33; :: thesis: verum