let L be Semilattice; :: 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;
A2: 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;
thus downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2) by Th61; :: according to XBOOLE_0:def 10 :: thesis: downarrow (D1 "/\" D2) c= downarrow ((downarrow D1) "/\" (downarrow D2))
let q be set ; :: 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
A3: q = s and
A4: ex z being Element of L st
( s <= z & z in D1 "/\" D2 ) by A1;
consider x being Element of L such that
A5: ( s <= x & x in D1 "/\" D2 ) by A4;
consider a, b being Element of L such that
A6: ( x = a "/\" b & a in D1 & b in D2 ) by A5;
( D1 is Subset of (downarrow D1) & D2 is Subset of (downarrow D2) ) by WAYBEL_0:16;
then x in (downarrow D1) "/\" (downarrow D2) by A6;
hence q in downarrow ((downarrow D1) "/\" (downarrow D2)) by A2, A3, A5; :: thesis: verum