let L be transitive antisymmetric with_suprema RelStr ; for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)
let D1, D2 be Subset of L; downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)
A1:
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;
let y be object ; TARSKI:def 3 ( not y in downarrow ((downarrow D1) "\/" (downarrow D2)) or y in downarrow (D1 "\/" D2) )
assume
y in downarrow ((downarrow D1) "\/" (downarrow D2))
; y in downarrow (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 (downarrow D1) "\/" (downarrow D2) )
by A1;
consider x1 being Element of L such that
A4:
x <= x1
and
A5:
x1 in (downarrow D1) "\/" (downarrow D2)
by A3;
consider a, b being Element of L such that
A6:
x1 = a "\/" b
and
A7:
a in downarrow D1
and
A8:
b in downarrow D2
by A5;
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;
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;
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;
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:
( downarrow (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:14;
a1 "\/" b1 in D1 "\/" D2
by A16, A12;
hence
y in downarrow (D1 "\/" D2)
by A2, A17; verum