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 object ; :: 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 and
A4: ex y being Element of R st
( x >= y & y in F ) by A1;
consider y being Element of R such that
A5: x >= y and
A6: y in F by A4;
A7: uparrow y in { (uparrow z) where z is Element of R : z in F } by A6;
x in uparrow y by A5, WAYBEL_0:18;
hence a in union { (uparrow z) where z is Element of R : z in F } by A3, A7, 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 object ; :: 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
A8: a in X and
A9: 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
A10: X = uparrow x and
A11: x in F by A9;
reconsider y = a as Element of R by A8, A10;
y >= x by A8, A10, WAYBEL_0:18;
hence a in uparrow F by A1, A11; :: 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 object ; :: 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
A12: a = x and
A13: ex y being Element of R st
( x <= y & y in F ) by A2;
consider y being Element of R such that
A14: x <= y and
A15: y in F by A13;
A16: downarrow y in { (downarrow z) where z is Element of R : z in F } by A15;
x in downarrow y by A14, WAYBEL_0:17;
hence a in union { (downarrow z) where z is Element of R : z in F } by A12, A16, TARSKI:def 4; :: thesis: verum
end;
hereby :: according to TARSKI:def 3 :: thesis: verum
let a be object ; :: 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
A17: a in X and
A18: 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
A19: X = downarrow x and
A20: x in F by A18;
reconsider y = a as Element of R by A17, A19;
y <= x by A17, A19, WAYBEL_0:17;
hence a in downarrow F by A2, A20; :: thesis: verum
end;