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 Def16;
hence latt L,P = (latt (L .: ),(P .: )) .: ; :: thesis: verum