let R be non empty Poset; :: thesis: for A, B being ManySortedSet of the carrier of R
for OR being ManySortedRelation of A,B st OR is os-compatible holds
OR is OrderSortedSet of R
let A, B be ManySortedSet of the carrier of R; :: thesis: for OR being ManySortedRelation of A,B st OR is os-compatible holds
OR is OrderSortedSet of R
let OR be ManySortedRelation of A,B; :: thesis: ( OR is os-compatible implies OR is OrderSortedSet of R )
set OR1 = OR;
assume A1: OR is os-compatible ; :: thesis: OR is OrderSortedSet of R
OR is order-sorted

proof

let s1, s2 be Element of R; :: according to OSALG_1:def 18 :: thesis: ( not s1 <= s2 or OR . s1 c= OR . s2 )
assume A2: s1 <= s2 ; :: thesis: OR . s1 c= OR . s2
for x, y being set st [x,y] in OR . s1 holds
[x,y] in OR . s2

proof

let x, y be set ; :: thesis: ( [x,y] in OR . s1 implies [x,y] in OR . s2 )
assume A3: [x,y] in OR . s1 ; :: thesis: [x,y] in OR . s2
( x in A . s1 & y in B . s1 ) by A3, ZFMISC_1:106;
hence [x,y] in OR . s2 by A1, A2, A3, Def1; :: thesis: verum

end;

hence OR . s1 c= OR . s2 by RELAT_1:def 3; :: thesis: verum

end;

hence OR is OrderSortedSet of R ; :: thesis: verum