let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of L
for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X )
let X be Subset of L; :: thesis: for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X )
let x be Element of L; :: thesis: ( x is_>=_than X iff x is_>=_than downarrow X )
thus ( x is_>=_than X implies x is_>=_than downarrow X ) :: thesis: ( x is_>=_than downarrow X implies x is_>=_than X )

proof

assume A1: for y being Element of L st y in X holds
x >= y ; :: according to LATTICE3:def 9 :: thesis: x is_>=_than downarrow X
let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in downarrow X or y <= x )
assume y in downarrow X ; :: thesis: y <= x
then consider z being Element of L such that
A2: y <= z and
A3: z in X by Def15;
x >= z by A1, A3;
hence y <= x by A2, ORDERS_2:3; :: thesis: verum

end;

assume A4: for y being Element of L st y in downarrow X holds
x >= y ; :: according to LATTICE3:def 9 :: thesis: x is_>=_than X
let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in X or y <= x )
assume A5: y in X ; :: thesis: y <= x
y <= y ;
then y in downarrow X by A5, Def15;
hence y <= x by A4; :: thesis: verum