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 .: )) .:
consider o1, o2 being BinOp of P such that
A1: ( o1 = H₂(L) || P & o2 = H₃(L) || P & latt L,P = LattStr(# P,o1,o2 #) ) by Def16;
consider o3, o4 being BinOp of (P .: ) such that
A2: ( o3 = H₂(L .: ) || (P .: ) & o4 = H₃(L .: ) || (P .: ) & latt (L .: ),(P .: ) = LattStr(# (P .: ),o3,o4 #) ) by Def16;
thus latt L,P = (latt (L .: ),(P .: )) .: by A1, A2; :: thesis: verum