let L be transitive RelStr ; :: thesis: for X being set
for x, y being Element of L st X is_<=_than x & x <= y holds
X is_<=_than y
let X be set ; :: thesis: for x, y being Element of L st X is_<=_than x & x <= y holds
X is_<=_than y
let x, y be Element of L; :: thesis: ( X is_<=_than x & x <= y implies X is_<=_than y )
assume that
A1: for y being Element of L st y in X holds
y <= x and
A2: x <= y ; :: according to LATTICE3:def 9 :: thesis: X is_<=_than y
let z be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not z in X or z <= y )
assume z in X ; :: thesis: z <= y
then z <= x by A1;
hence z <= y by A2, ORDERS_2:3; :: thesis: verum