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 8 :: thesis: X is_>=_than y
let z be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not z in X or y <= z )
assume z in X ; :: thesis: y <= z
then z >= x by A1;
hence y <= z by A2, ORDERS_2:3; :: thesis: verum