let Q be non empty unital QuasiNetStr ; :: thesis: ( Q is Quantale implies Q is BlikleNet )
assume A1: Q is Quantale ; :: thesis: Q is BlikleNet
then reconsider Q' = Q as Quantale ;
defpred S₁[ set ] means $1 in {} ;
A2: for c being Element of Q' holds not S₁[c] ;
A3: Bottom Q' = "\/" {} ,Q' by LATTICE3:50;
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 Q' ;
take a = a; :: thesis: for b being Element of Q' holds a [*] b = a
let b be Element of Q'; :: thesis: a [*] b = a
deffunc H₅( Element of Q') -> Element of the carrier of Q' = $1 [*] b;
{ H₅(c) where c is Element of Q' : S₁[c] } = {} from QUANTAL1:sch 2(A2);
hence a [*] b = a by A3, Def6; :: thesis: verum

end;

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

end;

then ( Q is non empty with_zero multMagma & Q is non empty Lattice-like complete right-distributive left-distributive QuasiNetStr ) ;
hence Q is BlikleNet by A1; :: thesis: verum