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 u [= FinMeet B,f holds
for x being Element of A st x in B holds
u [= f . x
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 u [= FinMeet B,f holds
for x being Element of A st x in B holds
u [= f . x
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 u [= FinMeet B,f holds
for x being Element of A st x in B holds
u [= f . x
let B be Finite_Subset of A; :: thesis: for f being Function of A,the carrier of L st u [= FinMeet B,f holds
for x being Element of A st x in B holds
u [= f . x
let f be Function of A,the carrier of L; :: thesis: ( u [= FinMeet B,f implies for x being Element of A st x in B holds
u [= f . x )
assume A1: u [= FinMeet B,f ; :: thesis: for x being Element of A st x in B holds
u [= f . x
let x be Element of A; :: thesis: ( x in B implies u [= f . x )
assume x in B ; :: thesis: u [= f . x
then FinMeet B,f [= f . x by Th55;
hence u [= f . x by A1, LATTICES:25; :: thesis: verum