let L be Lattice; :: thesis: for u being Element of L
for A being non empty set
for B being Element of Fin A
for f being Function of A, the carrier of L st B <> {} & ( 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; :: thesis: for A being non empty set
for B being Element of Fin A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let A be non empty set ; :: thesis: for B being Element of Fin A
for f being Function of A, the carrier of L st B <> {} & ( 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; :: thesis: for f being Function of A, the carrier of L st B <> {} & ( 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; :: thesis: ( B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) implies u [= FinMeet (B,f) )
assume that
A1: B <> {} and
A2: for x being Element of A st x in B holds
u [= f . x ; :: thesis: u [= FinMeet (B,f)
reconsider u9 = u as Element of (L .:) ;
reconsider f9 = f as Function of A, the carrier of (L .:) ;
for x being Element of A st x in B holds
f9 . x [= u9 by A2, Th38;
then FinJoin (B,f9) [= u9 by A1, Th32;
hence u [= FinMeet (B,f) by Th39; :: thesis: verum