let L be Lattice; :: thesis: for P being non empty ClosedSubset of L holds
( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P )
let P be non empty ClosedSubset of L; :: thesis: ( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P )
ex o1, o2 being BinOp of P st
( o1 = H₂(L) || P & o2 = H₃(L) || P & latt (L,P) = LattStr(# P,o1,o2 #) ) by Def14;
hence ( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P ) ; :: thesis: verum