let S be OrderSortedSign; :: thesis: for z being non empty set
for z1 being Element of z holds
( TrivialOSA S,z,z1 is non-empty & TrivialOSA S,z,z1 is monotone )
let z be non empty set ; :: thesis: for z1 being Element of z holds
( TrivialOSA S,z,z1 is non-empty & TrivialOSA S,z,z1 is monotone )
let z1 be Element of z; :: thesis: ( TrivialOSA S,z,z1 is non-empty & TrivialOSA S,z,z1 is monotone )
set A = TrivialOSA S,z,z1;
thus TrivialOSA S,z,z1 is non-empty :: thesis: TrivialOSA S,z,z1 is monotone

proof

the Sorts of (TrivialOSA S,z,z1) = ConstOSSet S,z by Def24;
then the Sorts of (TrivialOSA S,z,z1) is non-empty by Th15;
hence TrivialOSA S,z,z1 is non-empty by MSUALG_1:def 8; :: thesis: verum

end;

then reconsider A1 = TrivialOSA S,z,z1 as non-empty OSAlgebra of S ;
for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den o1,A1 c= Den o2,A1

proof

let o1, o2 be OperSymbol of S; :: thesis: ( o1 <= o2 implies Den o1,A1 c= Den o2,A1 )
assume o1 <= o2 ; :: thesis: Den o1,A1 c= Den o2,A1
then A1: ( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) by Def22;
A2: ( Den o1,(TrivialOSA S,z,z1) = (Args o1,(TrivialOSA S,z,z1)) --> z1 & Den o2,(TrivialOSA S,z,z1) = (Args o2,(TrivialOSA S,z,z1)) --> z1 ) by Def24;
A3: Args o1,(TrivialOSA S,z,z1) = ((the Sorts of (TrivialOSA S,z,z1) # ) * the Arity of S) . o1 by MSUALG_1:def 9
.= (the Sorts of (TrivialOSA S,z,z1) # ) . (the Arity of S . o1) by FUNCT_2:21
.= (the Sorts of (TrivialOSA S,z,z1) # ) . (the_arity_of o1) by MSUALG_1:def 6 ;
Args o2,(TrivialOSA S,z,z1) = ((the Sorts of (TrivialOSA S,z,z1) # ) * the Arity of S) . o2 by MSUALG_1:def 9
.= (the Sorts of (TrivialOSA S,z,z1) # ) . (the Arity of S . o2) by FUNCT_2:21
.= (the Sorts of (TrivialOSA S,z,z1) # ) . (the_arity_of o2) by MSUALG_1:def 6 ;
hence Den o1,A1 c= Den o2,A1 by A1, A2, A3, Th20, FUNCT_4:5; :: thesis: verum

end;

hence TrivialOSA S,z,z1 is monotone by Th27; :: thesis: verum