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 Q' = Q as Quantale ;
A1: Bottom Q' = "\/" {} ,Q' by LATTICE3:50;
A2: for c being Element of holds not S₁[c] ;
Q' is with_zero

proof

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

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

end;

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

end;

hence Q is BlikleNet ; :: thesis: verum