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

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