let N be sup-Semilattice; :: thesis: for A being Subset of N st subrelstr A is join-inheriting holds
A is directed
let A be Subset of N; :: thesis: ( subrelstr A is join-inheriting implies A is directed )
assume A1: subrelstr A is join-inheriting ; :: thesis: A is directed
let x, y be Element of N; :: according to WAYBEL_0:def 1 :: thesis: ( not x in A or not y in A or ex b₁ being Element of the carrier of N st
( b₁ in A & x <= b₁ & y <= b₁ ) )
assume A2: ( x in A & y in A ) ; :: thesis: ex b₁ being Element of the carrier of N st
( b₁ in A & x <= b₁ & y <= b₁ )
take x "\/" y ; :: thesis: ( x "\/" y in A & x <= x "\/" y & y <= x "\/" y )
A3: the carrier of (subrelstr A) = A by YELLOW_0:def 15;
ex_sup_of {x,y},N by YELLOW_0:20;
then sup {x,y} in the carrier of (subrelstr A) by A1, A2, A3;
hence x "\/" y in A by A3, YELLOW_0:41; :: thesis: ( x <= x "\/" y & y <= x "\/" y )
thus ( x <= x "\/" y & y <= x "\/" y ) by YELLOW_0:22; :: thesis: verum