set z1 = the Element of {{}};
take TrivialOSA (S,{{}}, the Element of {{}}) ; :: thesis: ( TrivialOSA (S,{{}}, the Element of {{}}) is monotone & TrivialOSA (S,{{}}, the Element of {{}}) is strict & TrivialOSA (S,{{}}, the Element of {{}}) is non-empty )
thus ( TrivialOSA (S,{{}}, the Element of {{}}) is monotone & TrivialOSA (S,{{}}, the Element of {{}}) is strict & TrivialOSA (S,{{}}, the Element of {{}}) is non-empty ) ; :: thesis: verum