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