let L be Lattice; :: thesis: for P being non empty ClosedSubset of L holds latt (L,P) = (latt ((L .:),(P .:))) .:
let P be non empty ClosedSubset of L; :: thesis: latt (L,P) = (latt ((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 #) ) & ex o3, o4 being BinOp of (P .:) st
( o3 = H₂(L .: ) || (P .:) & o4 = H₃(L .: ) || (P .:) & latt ((L .:),(P .:)) = LattStr(# (P .:),o3,o4 #) ) ) by Def14;
hence latt (L,P) = (latt ((L .:),(P .:))) .: ; :: thesis: verum