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