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:20;
C is os-compatible

proof

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 ;
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 A2: ( 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 )
reconsider O1 = the Sorts of U1 as OrderSortedSet of by OSALG_1:17;
A3: O1 . s3 c= O1 . s4 by A1, OSALG_1:def 18;
( 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 21;
hence ( [x,y] in C . s1 iff [x,y] in C . s2 ) by A2, A3, ZFMISC_1:106; :: thesis: verum

end;

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