let L be with_infima Poset; :: thesis: for S being non empty full meet-inheriting SubRelStr of L
for x, y being Element of S
for a, b being Element of L st a = x & b = y holds
x "/\" y = a "/\" b
let S be non empty full meet-inheriting SubRelStr of L; :: thesis: for x, y being Element of S
for a, b being Element of L st a = x & b = y holds
x "/\" y = a "/\" b
let x, y be Element of S; :: thesis: for a, b being Element of L st a = x & b = y holds
x "/\" y = a "/\" b
let a, b be Element of L; :: thesis: ( a = x & b = y implies x "/\" y = a "/\" b )
assume A1: ( a = x & b = y ) ; :: thesis: x "/\" y = a "/\" b
A2: ex_inf_of {a,b},L by Th21;
then "/\" ({x,y},L) in the carrier of S by A1, Def16;
then A3: "/\" ({x,y},S) = "/\" ({x,y},L) by A1, A2, Th63;
a "/\" b = inf {a,b} by Th40;
hence x "/\" y = a "/\" b by A1, A3, Th40; :: thesis: verum