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