let S be OrderSortedSign; 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 ; 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; ( 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 V8()
by Th15;
hence
TrivialOSA (S,z,z1) is non-empty
by MSUALG_1:def 3; 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;
( 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
;
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;
verum
end;
hence
TrivialOSA (S,z,z1) is monotone
by Th27; verum