let L be Lattice; :: thesis: for A being non empty set
for B being Finite_Subset of
for f, g being Function of A,the carrier of L st B <> {} & f | B = g | B holds
FinMeet B,f = FinMeet B,g
let A be non empty set ; :: thesis: for B being Finite_Subset of
for f, g being Function of A,the carrier of L st B <> {} & f | B = g | B holds
FinMeet B,f = FinMeet B,g
let B be Finite_Subset of ; :: thesis: for f, g being Function of A,the carrier of L st B <> {} & f | B = g | B holds
FinMeet B,f = FinMeet B,g
let f, g be Function of A,the carrier of L; :: thesis: ( B <> {} & f | B = g | B implies FinMeet B,f = FinMeet B,g )
reconsider f' = f, g' = g as Function of A,the carrier of (L .: ) ;
A1: ( FinMeet B,f = FinJoin B,f' & FinMeet B,g = FinJoin B,g' ) ;
assume ( B <> {} & f | B = g | B ) ; :: thesis: FinMeet B,f = FinMeet B,g
hence FinMeet B,f = FinMeet B,g by A1, Th49; :: thesis: verum