let L be transitive antisymmetric with_suprema RelStr ; :: thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2)
let D1, D2 be Subset of L; :: thesis: uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2)
A1: uparrow (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:15;
A2: uparrow ((uparrow D1) "\/" (uparrow D2)) = { x where x is Element of L : ex t being Element of L st
( x >= t & t in (uparrow D1) "\/" (uparrow D2) ) } by WAYBEL_0:15;
A3: uparrow D1 = { s1 where s1 is Element of L : ex z being Element of L st
( s1 >= z & z in D1 ) } by WAYBEL_0:15;
A4: uparrow D2 = { s2 where s2 is Element of L : ex z being Element of L st
( s2 >= z & z in D2 ) } by WAYBEL_0:15;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in uparrow ((uparrow D1) "\/" (uparrow D2)) or y in uparrow (D1 "\/" D2) )
assume y in uparrow ((uparrow D1) "\/" (uparrow D2)) ; :: thesis: y in uparrow (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 (uparrow D1) "\/" (uparrow D2) ) by A2;
consider x1 being Element of L such that
A7: x >= x1 and
A8: x1 in (uparrow D1) "\/" (uparrow D2) by A6;
consider a, b being Element of L such that
A9: x1 = a "\/" b and
A10: ( a in uparrow D1 & b in uparrow 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 uparrow (D1 "\/" D2) by A1, A5, A17; :: thesis: verum