let S be OrderSortedSign; for U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1
let U1 be non-empty OSAlgebra of S; [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1
reconsider C = [| the Sorts of U1, the Sorts of U1|] as MSCongruence of U1 by MSUALG_5:18;
C is os-compatible
proof
reconsider O1 = the
Sorts of
U1 as
OrderSortedSet of
S by OSALG_1:17;
let s1,
s2 be
Element of
S;
OSALG_4:def 1 ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in C . s1 iff [x,y] in C . s2 ) )
assume A1:
s1 <= s2
;
for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in C . s1 iff [x,y] in C . s2 )
reconsider s3 =
s1,
s4 =
s2 as
Element of
S ;
A2:
O1 . s3 c= O1 . s4
by A1, OSALG_1:def 16;
A3:
(
C . s1 = [:( the Sorts of U1 . s1),( the Sorts of U1 . s1):] &
C . s2 = [:( the Sorts of U1 . s2),( the Sorts of U1 . s2):] )
by PBOOLE:def 16;
let x,
y be
set ;
( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in C . s1 iff [x,y] in C . s2 ) )
assume
(
x in the
Sorts of
U1 . s1 &
y in the
Sorts of
U1 . s1 )
;
( [x,y] in C . s1 iff [x,y] in C . s2 )
hence
(
[x,y] in C . s1 iff
[x,y] in C . s2 )
by A2, A3, ZFMISC_1:87;
verum
end;
hence
[| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1
by Def2; verum