let A be non empty set ; :: thesis: for B being Element of Fin 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 Element of Fin 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 :: thesis: for x being Element of A st x in B holds
FinMeet (B,f) [= g . x

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, Th41; :: thesis: verum

end;

hence FinMeet (B,f) [= FinMeet (B,g) by Th59; :: thesis: verum