deffunc H4( Subset of X, Subset of X) -> Element of bool X = $1 \/ $2;
consider j being BinOp of (bool X) such that
A1:
for x, y being Subset of X holds j . (x,y) = H4(x,y)
from BINOP_1:sch 4();
deffunc H5( Subset of X, Subset of X) -> Element of bool X = $1 /\ $2;
consider m being BinOp of (bool X) such that
A2:
for x, y being Subset of X holds m . (x,y) = H5(x,y)
from BINOP_1:sch 4();
take
LattStr(# (bool X),j,m #)
; ( the carrier of LattStr(# (bool X),j,m #) = bool X & ( for Y, Z being Subset of X holds
( the L_join of LattStr(# (bool X),j,m #) . (Y,Z) = Y \/ Z & the L_meet of LattStr(# (bool X),j,m #) . (Y,Z) = Y /\ Z ) ) )
thus
( the carrier of LattStr(# (bool X),j,m #) = bool X & ( for Y, Z being Subset of X holds
( the L_join of LattStr(# (bool X),j,m #) . (Y,Z) = Y \/ Z & the L_meet of LattStr(# (bool X),j,m #) . (Y,Z) = Y /\ Z ) ) )
by A1, A2; verum