scheme :: MULTOP_1:sch 2
TriOpEx{ F1() -> non empty set , P1[ Element of F1(), Element of F1(), Element of F1(), Element of F1()] } :
ex o being TriOp of F1() st
for a, b, c being Element of F1() holds P1[a,b,c,o . (a,b,c)]
provided
A1: for x, y, z being Element of F1() ex t being Element of F1() st P1[x,y,z,t]