defpred S₁[ set ] means $1 in {} ;
let Q be non empty unital QuasiNetStr ; :: thesis: ( Q is Quantale implies Q is BlikleNet )
assume Q is Quantale ; :: thesis: Q is BlikleNet
then reconsider Q9 = Q as Quantale ;
A1: Bottom Q9 = "\/" ({},Q9) by LATTICE3:49;
A2: for c being Element of Q9 holds not S₁[c] ;
Q9 is with_zero

proof

hereby :: according to QUANTAL1:def 2,QUANTAL1:def 4 :: thesis: Q9 is with_right-zero

reconsider a = Bottom Q9 as Element of Q9 ;
take a = a; :: thesis: for b being Element of Q9 holds a [*] b = a
let b be Element of Q9; :: thesis: a [*] b = a
deffunc H₅( Element of Q9) -> Element of the carrier of Q9 = $1 [*] b;
{ H₅(c) where c is Element of Q9 : S₁[c] } = {} from QUANTAL1:sch 2(A2);
hence a [*] b = a by A1, Def6; :: thesis: verum

end;

take Bottom Q9 ; :: according to QUANTAL1:def 3 :: thesis: for a being Element of Q9 holds a * (Bottom Q9) = Bottom Q9
let a be Element of Q9; :: thesis: a * (Bottom Q9) = Bottom Q9
deffunc H₅( Element of Q9) -> Element of the carrier of Q9 = a [*] $1;
{ H₅(c) where c is Element of Q9 : S₁[c] } = {} from QUANTAL1:sch 2(A2);
hence a * (Bottom Q9) = Bottom Q9 by A1, Def5; :: thesis: verum

end;

hence Q is BlikleNet ; :: thesis: verum