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 Def24;
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 8; :: thesis: TrivialOSA S,z,z1 is monotone
reconsider A1 = TrivialOSA S,z,z1 as non-empty OSAlgebra of S by A1, MSUALG_1:def 8;
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 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 ;
A3: 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 ;
assume o1 <= o2 ; :: thesis: Den o1,A1 c= Den o2,A1
then A4: the_arity_of o1 <= the_arity_of o2 by Def22;
( 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;
hence Den o1,A1 c= Den o2,A1 by A4, A2, A3, Th20, FUNCT_4:5; :: thesis: verum

end;

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