let L be non empty RelStr ; :: thesis: for S being Subset of L holds

( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S )

let S be Subset of L; :: thesis: ( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S )

thus ( S is join-closed implies for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S ) :: thesis: ( ( for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S ) implies S is join-closed )

sup {x,y} in S ; :: thesis: S is join-closed

hence S is join-closed ; :: thesis: verum

( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S )

let S be Subset of L; :: thesis: ( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S )

thus ( S is join-closed implies for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S ) :: thesis: ( ( for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S ) implies S is join-closed )

proof

assume A5:
for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
assume
S is join-closed
; :: thesis: for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S

then A1: subrelstr S is join-inheriting ;

let x, y be Element of L; :: thesis: ( x in S & y in S & ex_sup_of {x,y},L implies sup {x,y} in S )

assume that

A2: x in S and

A3: y in S and

A4: ex_sup_of {x,y},L ; :: thesis: sup {x,y} in S

the carrier of (subrelstr S) = S by YELLOW_0:def 15;

hence sup {x,y} in S by A1, A2, A3, A4; :: thesis: verum

end;sup {x,y} in S

then A1: subrelstr S is join-inheriting ;

let x, y be Element of L; :: thesis: ( x in S & y in S & ex_sup_of {x,y},L implies sup {x,y} in S )

assume that

A2: x in S and

A3: y in S and

A4: ex_sup_of {x,y},L ; :: thesis: sup {x,y} in S

the carrier of (subrelstr S) = S by YELLOW_0:def 15;

hence sup {x,y} in S by A1, A2, A3, A4; :: thesis: verum

sup {x,y} in S ; :: thesis: S is join-closed

now :: thesis: for x, y being Element of L st x in the carrier of (subrelstr S) & y in the carrier of (subrelstr S) & ex_sup_of {x,y},L holds

sup {x,y} in the carrier of (subrelstr S)

then
subrelstr S is join-inheriting
;sup {x,y} in the carrier of (subrelstr S)

let x, y be Element of L; :: thesis: ( x in the carrier of (subrelstr S) & y in the carrier of (subrelstr S) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (subrelstr S) )

assume that

A6: x in the carrier of (subrelstr S) and

A7: y in the carrier of (subrelstr S) and

A8: ex_sup_of {x,y},L ; :: thesis: sup {x,y} in the carrier of (subrelstr S)

the carrier of (subrelstr S) = S by YELLOW_0:def 15;

hence sup {x,y} in the carrier of (subrelstr S) by A5, A6, A7, A8; :: thesis: verum

end;assume that

A6: x in the carrier of (subrelstr S) and

A7: y in the carrier of (subrelstr S) and

A8: ex_sup_of {x,y},L ; :: thesis: sup {x,y} in the carrier of (subrelstr S)

the carrier of (subrelstr S) = S by YELLOW_0:def 15;

hence sup {x,y} in the carrier of (subrelstr S) by A5, A6, A7, A8; :: thesis: verum

hence S is join-closed ; :: thesis: verum