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