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;

hereby :: according to TARSKI:def 3 :: thesis: X c= 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;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in uparrow X )
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