let L be non empty transitive RelStr ; :: thesis: for x, y being Element of L st x <= y holds

uparrow y c= uparrow x

let x, y be Element of L; :: thesis: ( x <= y implies uparrow y c= uparrow x )

assume A1: x <= y ; :: thesis: uparrow y c= uparrow x

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in uparrow y or z in uparrow x )

assume A2: z in uparrow y ; :: thesis: z in uparrow x

then reconsider z = z as Element of L ;

y <= z by A2, Th18;

then x <= z by A1, ORDERS_2:3;

hence z in uparrow x by Th18; :: thesis: verum

uparrow y c= uparrow x

let x, y be Element of L; :: thesis: ( x <= y implies uparrow y c= uparrow x )

assume A1: x <= y ; :: thesis: uparrow y c= uparrow x

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in uparrow y or z in uparrow x )

assume A2: z in uparrow y ; :: thesis: z in uparrow x

then reconsider z = z as Element of L ;

y <= z by A2, Th18;

then x <= z by A1, ORDERS_2:3;

hence z in uparrow x by Th18; :: thesis: verum