let L be with_suprema Poset; :: thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2)
let D1, D2 be Subset of L; :: thesis: uparrow ((uparrow D1) "\/" (uparrow D2)) = 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;
thus uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2) by Th34; :: according to XBOOLE_0:def 10 :: thesis: uparrow (D1 "\/" D2) c= uparrow ((uparrow D1) "\/" (uparrow D2))
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in uparrow (D1 "\/" D2) or q in uparrow ((uparrow D1) "\/" (uparrow D2)) )
assume q in uparrow (D1 "\/" D2) ; :: thesis: q in uparrow ((uparrow D1) "\/" (uparrow D2))
then consider s being Element of L such that
A2: q = s and
A3: ex z being Element of L st
( s >= z & z in D1 "\/" D2 ) by A1;
A4: 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;
A5: ( D1 is Subset of (uparrow D1) & D2 is Subset of (uparrow D2) ) by WAYBEL_0:16;
consider x being Element of L such that
A6: s >= x and
A7: x in D1 "\/" D2 by A3;
ex a, b being Element of L st
( x = a "\/" b & a in D1 & b in D2 ) by A7;
then x in (uparrow D1) "\/" (uparrow D2) by A5;
hence q in uparrow ((uparrow D1) "\/" (uparrow D2)) by A4, A2, A6; :: thesis: verum