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 )

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

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 A4:
for y being Element of L st y in uparrow X holds
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;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

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