let L be reflexive RelStr ; :: thesis: for X being Subset of L holds

( X c= downarrow X & X c= uparrow X )

let X be Subset of L; :: thesis: ( X c= downarrow X & X c= uparrow X )

A1: the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;

assume A3: x in X ; :: thesis: x in uparrow X

then reconsider y = x as Element of L ;

[y,y] in the InternalRel of L by A1, A3, RELAT_2:def 1;

then y <= y by ORDERS_2:def 5;

hence x in uparrow X by A3, Def16; :: thesis: verum

( X c= downarrow X & X c= uparrow X )

let X be Subset of L; :: thesis: ( X c= downarrow X & X c= uparrow X )

A1: the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;

hereby :: according to TARSKI:def 3 :: thesis: X c= uparrow X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in uparrow X )let x be object ; :: thesis: ( x in X implies x in downarrow X )

assume A2: x in X ; :: thesis: x in downarrow X

then reconsider y = x as Element of L ;

[y,y] in the InternalRel of L by A1, A2, RELAT_2:def 1;

then y <= y by ORDERS_2:def 5;

hence x in downarrow X by A2, Def15; :: thesis: verum

end;assume A2: x in X ; :: thesis: x in downarrow X

then reconsider y = x as Element of L ;

[y,y] in the InternalRel of L by A1, A2, RELAT_2:def 1;

then y <= y by ORDERS_2:def 5;

hence x in downarrow X by A2, Def15; :: thesis: verum

assume A3: x in X ; :: thesis: x in uparrow X

then reconsider y = x as Element of L ;

[y,y] in the InternalRel of L by A1, A3, RELAT_2:def 1;

then y <= y by ORDERS_2:def 5;

hence x in uparrow X by A3, Def16; :: thesis: verum