let L be non empty transitive RelStr ; :: thesis: for x, y being Element of L st x <= y holds
downarrow x c= downarrow y
let x, y be Element of L; :: thesis: ( x <= y implies downarrow x c= downarrow y )
assume A1: x <= y ; :: thesis: downarrow x c= downarrow y
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in downarrow x or z in downarrow y )
assume A2: z in downarrow x ; :: thesis: z in downarrow y
then reconsider z = z as Element of L ;
z <= x by A2, Th17;
then z <= y by A1, ORDERS_2:3;
hence z in downarrow y by Th17; :: thesis: verum