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 Def16;
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