defpred S_{1}[ 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_{1}[c]
;

Q9 is with_zero

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

Q9 is with_zero

proof

let a be Element of Q9; :: thesis: a * (Bottom Q9) = Bottom Q9

deffunc H_{5}( Element of Q9) -> Element of the carrier of Q9 = a [*] $1;

{ H_{5}(c) where c is Element of Q9 : S_{1}[c] } = {}
from QUANTAL1:sch 2(A2);

hence a * (Bottom Q9) = Bottom Q9 by A1, Def5; :: thesis: verum

end;

hence
Q is BlikleNet
; :: thesis: verumhereby :: according to QUANTAL1:def 2,QUANTAL1:def 4 :: thesis: Q9 is with_right-zero

take
Bottom Q9
; :: according to QUANTAL1:def 3 :: thesis: for a being Element of Q9 holds a * (Bottom Q9) = Bottom Q9reconsider 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_{5}( Element of Q9) -> Element of the carrier of Q9 = $1 [*] b;

{ H_{5}(c) where c is Element of Q9 : S_{1}[c] } = {}
from QUANTAL1:sch 2(A2);

hence a [*] b = a by A1, Def6; :: thesis: verum

end;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

{ H

hence a [*] b = a by A1, Def6; :: thesis: verum

let a be Element of Q9; :: thesis: a * (Bottom Q9) = Bottom Q9

deffunc H

{ H

hence a * (Bottom Q9) = Bottom Q9 by A1, Def5; :: thesis: verum