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