let L be with_suprema Poset; :: thesis: for S being non empty full join-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 join-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_sup_of {a,b},L by Th20;
then "\/" ({x,y},L) in the carrier of S by A1, Def17;
then A3: "\/" ({x,y},S) = "\/" ({x,y},L) by A1, A2, Th64;
a "\/" b = sup {a,b} by Th41;
hence x "\/" y = a "\/" b by A1, A3, Th41; :: thesis: verum