let L be transitive antisymmetric with_suprema RelStr ; :: thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)
let D1, D2 be Subset of L; :: thesis: downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)
A1: downarrow (D1 "\/" D2) = { s where s is Element of L : ex z being Element of L st
( s <= z & z in D1 "\/" D2 ) } by WAYBEL_0:14;
A2: downarrow ((downarrow D1) "\/" (downarrow D2)) = { x where x is Element of L : ex t being Element of L st
( x <= t & t in (downarrow D1) "\/" (downarrow D2) ) } by WAYBEL_0:14;
A3: downarrow D1 = { s1 where s1 is Element of L : ex z being Element of L st
( s1 <= z & z in D1 ) } by WAYBEL_0:14;
A4: downarrow D2 = { s2 where s2 is Element of L : ex z being Element of L st
( s2 <= z & z in D2 ) } by WAYBEL_0:14;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in downarrow ((downarrow D1) "\/" (downarrow D2)) or y in downarrow (D1 "\/" D2) )
assume y in downarrow ((downarrow D1) "\/" (downarrow D2)) ; :: thesis: y in downarrow (D1 "\/" D2)
then consider x being Element of L such that
A5: y = x and
A6: ex t being Element of L st
( x <= t & t in (downarrow D1) "\/" (downarrow D2) ) by A2;
consider x1 being Element of L such that
A7: x <= x1 and
A8: x1 in (downarrow D1) "\/" (downarrow D2) by A6;
consider a, b being Element of L such that
A9: x1 = a "\/" b and
A10: ( a in downarrow D1 & b in downarrow D2 ) by A8;
consider A1 being Element of L such that
A11: a = A1 and
A12: ex z being Element of L st
( A1 <= z & z in D1 ) by A3, A10;
consider B1 being Element of L such that
A13: b = B1 and
A14: ex z being Element of L st
( B1 <= z & z in D2 ) by A4, A10;
consider a1 being Element of L such that
A15: ( A1 <= a1 & a1 in D1 ) by A12;
consider b1 being Element of L such that
A16: ( B1 <= b1 & b1 in D2 ) by A14;
x1 <= a1 "\/" b1 by A9, A11, A13, A15, A16, YELLOW_3:3;
then A17: x <= a1 "\/" b1 by A7, ORDERS_2:26;
a1 "\/" b1 in D1 "\/" D2 by A15, A16;
hence y in downarrow (D1 "\/" D2) by A1, A5, A17; :: thesis: verum