let L be Lattice; :: thesis: for P being non empty ClosedSubset of L
for p, q being Element of L
for p', q' being Element of (latt L,P) st p = p' & q = q' holds
( p "\/" q = p' "\/" q' & p "/\" q = p' "/\" q' )
let P be non empty ClosedSubset of L; :: thesis: for p, q being Element of L
for p', q' being Element of (latt L,P) st p = p' & q = q' holds
( p "\/" q = p' "\/" q' & p "/\" q = p' "/\" q' )
let p, q be Element of L; :: thesis: for p', q' being Element of (latt L,P) st p = p' & q = q' holds
( p "\/" q = p' "\/" q' & p "/\" q = p' "/\" q' )
let p', q' be Element of (latt L,P); :: thesis: ( p = p' & q = q' implies ( p "\/" q = p' "\/" q' & p "/\" q = p' "/\" q' ) )
assume A1:
( p = p' & q = q' )
; :: thesis: ( p "\/" q = p' "\/" q' & p "/\" q = p' "/\" q' )
consider o1, o2 being BinOp of P such that
A2:
( o1 = H2(L) || P & o2 = H3(L) || P & latt L,P = LattStr(# P,o1,o2 #) )
by Def16;
A3:
( dom o1 = [:P,P:] & dom o2 = [:P,P:] & [p',q'] in [:P,P:] )
by A2, FUNCT_2:def 1;
hence
p "\/" q = p' "\/" q'
by A1, A2, FUNCT_1:70; :: thesis: p "/\" q = p' "/\" q'
thus
p "/\" q = p' "/\" q'
by A1, A2, A3, FUNCT_1:70; :: thesis: verum