consider z being non empty set ;
consider z1 being Element of z;
take TrivialOSA S,z,z1 ; :: thesis: ( TrivialOSA S,z,z1 is monotone & TrivialOSA S,z,z1 is strict & TrivialOSA S,z,z1 is non-empty )
thus ( TrivialOSA S,z,z1 is monotone & TrivialOSA S,z,z1 is strict & TrivialOSA S,z,z1 is non-empty ) by Th29; :: thesis: verum