let L be Lattice; :: thesis: for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin (B,f)
let u be Element of L; :: thesis: for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin (B,f)
let A be non empty set ; :: thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin (B,f)
let B be Finite_Subset of A; :: thesis: for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin (B,f)
let f be Function of A, the carrier of L; :: thesis: ( ex x being Element of A st
( x in B & u [= f . x ) implies u [= FinJoin (B,f) )
given x being Element of A such that A1: x in B and
A2: u [= f . x ; :: thesis: u [= FinJoin (B,f)
f . x [= FinJoin (B,f) by A1, Th43;
then A3: (f . x) "\/" (FinJoin (B,f)) = FinJoin (B,f) by LATTICES:def 3;
then u "\/" (FinJoin (B,f)) = (u "\/" (f . x)) "\/" (FinJoin (B,f)) by LATTICES:def 5
.= FinJoin (B,f) by A2, A3, LATTICES:def 3 ;
hence u [= FinJoin (B,f) by LATTICES:def 3; :: thesis: verum