deffunc H₄( Subset of , Subset of ) -> Element of bool X = $1 \/ $2;
consider j being BinOp of bool X such that
A1: for x, y being Subset of holds j . x,y = H₄(x,y) from BINOP_1:sch 4();
deffunc H₅( Subset of , Subset of ) -> Element of bool X = $1 /\ $2;
consider m being BinOp of bool X such that
A2: for x, y being Subset of holds m . x,y = H₅(x,y) from BINOP_1:sch 4();
take LattStr(# (bool X),j,m #) ; :: thesis: ( the carrier of LattStr(# (bool X),j,m #) = bool X & ( for Y, Z being Subset of 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 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; :: thesis: verum