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

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

thus
I c= I "\/" I
by YELLOW_4:13; :: thesis: verum
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;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