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 uparrow X )
let X be Subset of L; :: thesis: for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X )
let x be Element of L; :: thesis: ( x is_<=_than X iff x is_<=_than uparrow X )
thus ( x is_<=_than X implies x is_<=_than uparrow X ) :: thesis: ( x is_<=_than uparrow 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 8 :: thesis: x is_<=_than uparrow X
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in uparrow X or x <= y )
assume y in uparrow X ; :: thesis: x <= y
then consider z being Element of L such that
A2: y >= z and
A3: z in X by Def16;
x <= z by A1, A3;
hence x <= y by A2, ORDERS_2:3; :: thesis: verum

end;

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