let S be OrderSortedSign; :: thesis: 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; :: thesis: [| 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; :: according to OSALG_4:def 1 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: ( [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; :: thesis: verum

end;

hence [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1 by Def2; :: thesis: verum