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 ((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;
let y be object ; :: 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
A2: y = x and
A3: ex t being Element of L st
( x >= t & t in (uparrow D1) "\/" (uparrow D2) ) by A1;
consider x1 being Element of L such that
A4: x >= x1 and
A5: x1 in (uparrow D1) "\/" (uparrow D2) by A3;
consider a, b being Element of L such that
A6: x1 = a "\/" b and
A7: a in uparrow D1 and
A8: b in uparrow D2 by A5;
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;
then consider B1 being Element of L such that
A9: b = B1 and
A10: ex z being Element of L st
( B1 >= z & z in D2 ) by A8;
consider b1 being Element of L such that
A11: B1 >= b1 and
A12: b1 in D2 by A10;
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;
then consider A1 being Element of L such that
A13: a = A1 and
A14: ex z being Element of L st
( A1 >= z & z in D1 ) by A7;
consider a1 being Element of L such that
A15: A1 >= a1 and
A16: a1 in D1 by A14;
x1 >= a1 "\/" b1 by A6, A13, A9, A15, A11, YELLOW_3:3;
then A17: ( uparrow (D1 "\/" D2) = { s where s is Element of L : ex z being Element of L st
( s >= z & z in D1 "\/" D2 ) } & x >= a1 "\/" b1 ) by A4, ORDERS_2:3, WAYBEL_0:15;
a1 "\/" b1 in D1 "\/" D2 by A16, A12;
hence y in uparrow (D1 "\/" D2) by A2, A17; :: thesis: verum