let L be with_suprema Poset; :: thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2)
let D1, D2 be Subset of L; :: thesis: downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2)
A1: downarrow (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:14;
thus downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2) by Th32; :: according to XBOOLE_0:def 10 :: thesis: downarrow (D1 "\/" D2) c= downarrow ((downarrow D1) "\/" (downarrow D2))
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in downarrow (D1 "\/" D2) or q in downarrow ((downarrow D1) "\/" (downarrow D2)) )
assume q in downarrow (D1 "\/" D2) ; :: thesis: q in downarrow ((downarrow D1) "\/" (downarrow 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: 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;
A5: ( D1 is Subset of (downarrow D1) & D2 is Subset of (downarrow 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 (downarrow D1) "\/" (downarrow D2) by A5;
hence q in downarrow ((downarrow D1) "\/" (downarrow D2)) by A4, A2, A6; :: thesis: verum