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 )
( [:P,P:] c= [:H₁(L),H₁(L):] & dom H₂(L) = [:H₁(L),H₁(L):] & dom H₃(L) = [:H₁(L),H₁(L):] ) by FUNCT_2:def 1;
then A1: ( dom (H₂(L) || P) = [:P,P:] & dom (H₃(L) || P) = [:P,P:] ) by RELAT_1:91;
rng (H₂(L) || P) c= P

proof

let x be set ; :: 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 set such that
A2: ( y in [:P,P:] & x = (H₂(L) || P) . y ) by A1, FUNCT_1:def 5;
consider p1, p2 being Element of P such that
A3: y = [p1,p2] by A2, DOMAIN_1:9;
x = p1 "\/" p2 by A1, A2, A3, FUNCT_1:70;
hence x in P by LATTICE4:def 10; :: thesis: verum

end;

hence H₂(L) || P is BinOp of P by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: the L_meet of L || P is BinOp of P
rng (H₃(L) || P) c= P

proof

let x be set ; :: 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 set such that
A4: ( y in [:P,P:] & x = (H₃(L) || P) . y ) by A1, FUNCT_1:def 5;
consider p1, p2 being Element of P such that
A5: y = [p1,p2] by A4, DOMAIN_1:9;
x = p1 "/\" p2 by A1, A4, A5, FUNCT_1:70;
hence x in P by LATTICE4:def 10; :: thesis: verum

end;

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