let L be Lattice; :: thesis: for P being non empty ClosedSubset of L holds
( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P )
let P be non empty ClosedSubset of L; :: thesis: ( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P )
dom H₂(L) = [:H₁(L),H₁(L):] by FUNCT_2:def 1;
then A1: dom (H₂(L) || P) = [:P,P:] by RELAT_1:62;
rng (H₂(L) || P) c= P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (H₂(L) || P) or x in P )
assume x in rng (H₂(L) || P) ; :: thesis: x in P
then consider y being object such that
A2: y in [:P,P:] and
A3: x = (H₂(L) || P) . y by A1, FUNCT_1:def 3;
consider p1, p2 being Element of P such that
A4: y = [p1,p2] by A2, DOMAIN_1:1;
x = p1 "\/" p2 by A1, A3, A4, FUNCT_1:47;
hence x in P by LATTICES:def 25; :: thesis: verum

end;

hence H₂(L) || P is BinOp of P by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: the L_meet of L || P is BinOp of P
dom H₃(L) = [:H₁(L),H₁(L):] by FUNCT_2:def 1;
then A5: dom (H₃(L) || P) = [:P,P:] by RELAT_1:62;
rng (H₃(L) || P) c= P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (H₃(L) || P) or x in P )
assume x in rng (H₃(L) || P) ; :: thesis: x in P
then consider y being object such that
A6: y in [:P,P:] and
A7: x = (H₃(L) || P) . y by A5, FUNCT_1:def 3;
consider p1, p2 being Element of P such that
A8: y = [p1,p2] by A6, DOMAIN_1:1;
x = p1 "/\" p2 by A5, A7, A8, FUNCT_1:47;
hence x in P by LATTICES:def 24; :: thesis: verum

end;

hence the L_meet of L || P is BinOp of P by A5, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum