let L be Lattice; :: thesis: for A being non empty set
for B being Element of Fin A
for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
let A be non empty set ; :: thesis: for B being Element of Fin A
for f, g being Function of A, the carrier of L st B <> {} & ( 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 f, g being Function of A, the carrier of L st B <> {} & ( 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: ( B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) implies FinMeet (B,f) [= FinMeet (B,g) )
assume that
A1: B <> {} and
A2: 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 A3: x in B ; :: thesis: FinMeet (B,f) [= g . x
then f . x [= g . x by A2;
hence FinMeet (B,f) [= g . x by A3, Th41; :: thesis: verum

end;

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