let L be Lattice; :: thesis: for A being non empty set
for x being Element of A
for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f)
let A be non empty set ; :: thesis: for x being Element of A
for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f)
let x be Element of A; :: thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f)
let B be Finite_Subset of A; :: thesis: for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f)
let f be Function of A, the carrier of L; :: thesis: ( x in B implies f . x [= FinJoin (B,f) )
assume x in B ; :: thesis: f . x [= FinJoin (B,f)
then (f . x) "\/" (FinJoin (B,f)) = FinJoin (B,f) by SETWISEO:22;
hence f . x [= FinJoin (B,f) by LATTICES:def 3; :: thesis: verum