let A be non empty set ; :: thesis: for B being Finite_Subset of A
for L being 1_Lattice
for f, g being Function of A,the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet B,f [= FinMeet B,g
let B be Finite_Subset of A; :: thesis: for L being 1_Lattice
for f, g being Function of A,the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet B,f [= FinMeet B,g
let L be 1_Lattice; :: thesis: for f, g being Function of A,the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet B,f [= FinMeet B,g
let f, g be Function of A,the carrier of L; :: thesis: ( ( for x being Element of A st x in B holds
f . x [= g . x ) implies FinMeet B,f [= FinMeet B,g )
assume A1: for x being Element of A st x in B holds
f . x [= g . x ; :: thesis: FinMeet B,f [= FinMeet B,g

now

let x be Element of A; :: thesis: ( x in B implies FinMeet B,f [= g . x )
assume A2: x in B ; :: thesis: FinMeet B,f [= g . x
then f . x [= g . x by A1;
hence FinMeet B,f [= g . x by A2, Th56; :: thesis: verum

end;

hence FinMeet B,f [= FinMeet B,g by Th76; :: thesis: verum