let L be sup-Semilattice; :: thesis: for I being directed lower Subset of L holds I "\/" I = I
let I be directed lower Subset of L; :: thesis: I "\/" I = I
thus I "\/" I c= I :: according to XBOOLE_0:def 10 :: thesis: I c= I "\/" I
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in I "\/" I or x in I )
assume x in I "\/" I ; :: thesis: x in I
then consider y, z being Element of L such that
A1: x = y "\/" z and
A2: ( y in I & z in I ) ;
consider t being Element of L such that
A3: t in I and
A4: ( t >= y & t >= z ) by A2, WAYBEL_0:def 1;
y "\/" z <= t by A4, YELLOW_0:22;
hence x in I by A1, A3, WAYBEL_0:def 19; :: thesis: verum
end;
thus I c= I "\/" I by YELLOW_4:13; :: thesis: verum