let R be non empty RelStr ; :: thesis: for F being Subset of R holds
( uparrow F = union { (uparrow x) where x is Element of R : x in F } & downarrow F = union { (downarrow x) where x is Element of R : x in F } )
let F be Subset of R; :: thesis: ( uparrow F = union { (uparrow x) where x is Element of R : x in F } & downarrow F = union { (downarrow x) where x is Element of R : x in F } )
A1: uparrow F = { x where x is Element of R : ex y being Element of R st
( x >= y & y in F ) } by WAYBEL_0:15;
A2: downarrow F = { x where x is Element of R : ex y being Element of R st
( x <= y & y in F ) } by WAYBEL_0:14;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: ( union { (uparrow x) where x is Element of R : x in F } c= uparrow F & downarrow F = union { (downarrow x) where x is Element of R : x in F } )

let a be set ; :: thesis: ( a in uparrow F implies a in union { (uparrow z) where z is Element of R : z in F } )
assume a in uparrow F ; :: thesis: a in union { (uparrow z) where z is Element of R : z in F }
then consider x being Element of R such that
A3: ( a = x & ex y being Element of R st
( x >= y & y in F ) ) by A1;
consider y being Element of R such that
A4: ( x >= y & y in F ) by A3;
( uparrow y in { (uparrow z) where z is Element of R : z in F } & x in uparrow y ) by A4, WAYBEL_0:18;
hence a in union { (uparrow z) where z is Element of R : z in F } by A3, TARSKI:def 4; :: thesis: verum

end;

hereby :: according to TARSKI:def 3 :: thesis: downarrow F = union { (downarrow x) where x is Element of R : x in F }

let a be set ; :: thesis: ( a in union { (uparrow x) where x is Element of R : x in F } implies a in uparrow F )
assume a in union { (uparrow x) where x is Element of R : x in F } ; :: thesis: a in uparrow F
then consider X being set such that
A5: ( a in X & X in { (uparrow x) where x is Element of R : x in F } ) by TARSKI:def 4;
consider x being Element of R such that
A6: ( X = uparrow x & x in F ) by A5;
reconsider y = a as Element of R by A5, A6;
y >= x by A5, A6, WAYBEL_0:18;
hence a in uparrow F by A1, A6; :: thesis: verum

end;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (downarrow x) where x is Element of R : x in F } c= downarrow F

let a be set ; :: thesis: ( a in downarrow F implies a in union { (downarrow z) where z is Element of R : z in F } )
assume a in downarrow F ; :: thesis: a in union { (downarrow z) where z is Element of R : z in F }
then consider x being Element of R such that
A7: ( a = x & ex y being Element of R st
( x <= y & y in F ) ) by A2;
consider y being Element of R such that
A8: ( x <= y & y in F ) by A7;
( downarrow y in { (downarrow z) where z is Element of R : z in F } & x in downarrow y ) by A8, WAYBEL_0:17;
hence a in union { (downarrow z) where z is Element of R : z in F } by A7, TARSKI:def 4; :: thesis: verum

end;

hereby :: according to TARSKI:def 3 :: thesis: verum

let a be set ; :: thesis: ( a in union { (downarrow x) where x is Element of R : x in F } implies a in downarrow F )
assume a in union { (downarrow x) where x is Element of R : x in F } ; :: thesis: a in downarrow F
then consider X being set such that
A9: ( a in X & X in { (downarrow x) where x is Element of R : x in F } ) by TARSKI:def 4;
consider x being Element of R such that
A10: ( X = downarrow x & x in F ) by A9;
reconsider y = a as Element of R by A9, A10;
y <= x by A9, A10, WAYBEL_0:17;
hence a in downarrow F by A2, A10; :: thesis: verum

end;