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);
the Sorts of (TrivialOSA (S,z,z1)) = ConstOSSet (S,z) by Def22;
then A1: the Sorts of (TrivialOSA (S,z,z1)) is non-empty by Th15;
hence TrivialOSA (S,z,z1) is non-empty by MSUALG_1:def 3; :: thesis: TrivialOSA (S,z,z1) is monotone
reconsider A1 = TrivialOSA (S,z,z1) as non-empty OSAlgebra of S by A1, MSUALG_1:def 3;
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) )
A2: Args (o1,(TrivialOSA (S,z,z1))) = (( the Sorts of (TrivialOSA (S,z,z1)) #) * the Arity of S) . o1 by MSUALG_1:def 4
.= ( the Sorts of (TrivialOSA (S,z,z1)) #) . ( the Arity of S . o1) by FUNCT_2:15
.= ( the Sorts of (TrivialOSA (S,z,z1)) #) . (the_arity_of o1) by MSUALG_1:def 1 ;
A3: Args (o2,(TrivialOSA (S,z,z1))) = (( the Sorts of (TrivialOSA (S,z,z1)) #) * the Arity of S) . o2 by MSUALG_1:def 4
.= ( the Sorts of (TrivialOSA (S,z,z1)) #) . ( the Arity of S . o2) by FUNCT_2:15
.= ( the Sorts of (TrivialOSA (S,z,z1)) #) . (the_arity_of o2) by MSUALG_1:def 1 ;
assume o1 <= o2 ; :: thesis: Den (o1,A1) c= Den (o2,A1)
then A4: the_arity_of o1 <= the_arity_of o2 ;
( 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 Def22;
hence Den (o1,A1) c= Den (o2,A1) by A4, A2, A3, Th20, FUNCT_4:4; :: thesis: verum

end;

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