let L be Lattice; :: thesis: for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let P be non empty ClosedSubset of L; :: thesis: for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p, q be Element of L; :: thesis: for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p9, q9 be Element of (latt (L,P)); :: thesis: ( p = p9 & q = q9 implies ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) )
assume A1: ( p = p9 & q = q9 ) ; :: thesis: ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
consider o1, o2 being BinOp of P such that
A2: o1 = H₂(L) || P and
A3: o2 = H₃(L) || P and
A4: latt (L,P) = LattStr(# P,o1,o2 #) by Def14;
A5: [p9,q9] in [:P,P:] by A4;
dom o1 = [:P,P:] by FUNCT_2:def 1;
hence p "\/" q = p9 "\/" q9 by A1, A2, A4, A5, FUNCT_1:47; :: thesis: p "/\" q = p9 "/\" q9
dom o2 = [:P,P:] by FUNCT_2:def 1;
hence p "/\" q = p9 "/\" q9 by A1, A3, A4, A5, FUNCT_1:47; :: thesis: verum