let L be non empty RelStr ; 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; ( 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 )
( ( 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
S is
join-closed
;
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;
( 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
;
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;
verum
end;
assume A5:
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
; S is join-closed
now 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)let x,
y be
Element of
L;
( 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
;
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;
verum end;
then
subrelstr S is join-inheriting
;
hence
S is join-closed
; verum