let A be non empty set ; :: thesis: for B being Finite_Subset of
for L being 1_Lattice
for f being Function of A,the carrier of L
for u being Element of st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet B,f
let B be Finite_Subset of ; :: thesis: for L being 1_Lattice
for f being Function of A,the carrier of L
for u being Element of 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; :: thesis: for f being Function of A,the carrier of L
for u being Element of 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; :: thesis: for u being Element of 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 ; :: thesis: ( ( for x being Element of A st x in B holds
u [= f . x ) implies u [= FinMeet B,f )
reconsider f' = f as Function of A,the carrier of (L .: ) ;
reconsider u' = u as Element of ;
assume for x being Element of A st x in B holds
u [= f . x ; :: thesis: u [= FinMeet B,f
then A1: for x being Element of A st x in B holds
f' . x [= u' by Th53;
L .: is 0_Lattice by Th64;
then FinJoin B,f' [= u' by A1, Th70;
hence u [= FinMeet B,f by Th54; :: thesis: verum