let A be non empty set ; for B being Element of Fin A
for L being 1_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let B be Element of Fin A; for L being 1_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let L be 1_Lattice; for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let f be Function of A, the carrier of L; for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let u be Element of L; ( ( for x being Element of A st x in B holds
u [= f . x ) implies u [= FinMeet (B,f) )
reconsider f9 = f as Function of A, the carrier of (L .:) ;
reconsider u9 = u as Element of (L .:) ;
assume
for x being Element of A st x in B holds
u [= f . x
; u [= FinMeet (B,f)
then A1:
for x being Element of A st x in B holds
f9 . x [= u9
by Th38;
L .: is 0_Lattice
by Th49;
then
FinJoin (B,f9) [= u9
by A1, Th54;
hence
u [= FinMeet (B,f)
by Th39; verum