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