let L be transitive antisymmetric with_infima RelStr ; for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2)
let D1, D2 be Subset of L; 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 ; TARSKI:def 3 ( not y in uparrow ((uparrow D1) "/\" (uparrow D2)) or y in uparrow (D1 "/\" D2) )
assume
y in uparrow ((uparrow D1) "/\" (uparrow D2))
; 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:2;
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; verum