let L be non empty RelStr ; :: thesis: for S being Subset of L holds
( S is sups-closed iff for X being Subset of S st ex_sup_of X,L holds
"\/" X,L in S )
let S be Subset of L; :: thesis: ( S is sups-closed iff for X being Subset of S st ex_sup_of X,L holds
"\/" X,L in S )
thus ( S is sups-closed implies for X being Subset of S st ex_sup_of X,L holds
"\/" X,L in S ) :: thesis: ( ( for X being Subset of S st ex_sup_of X,L holds
"\/" X,L in S ) implies S is sups-closed )

proof

assume S is sups-closed ; :: thesis: for X being Subset of S st ex_sup_of X,L holds
"\/" X,L in S
then A1: subrelstr S is sups-inheriting by Def4;
let X be Subset of S; :: thesis: ( ex_sup_of X,L implies "\/" X,L in S )
A2: X is Subset of (subrelstr S) by YELLOW_0:def 15;
assume ex_sup_of X,L ; :: thesis: "\/" X,L in S
then "\/" X,L in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def 19;
hence "\/" X,L in S by YELLOW_0:def 15; :: thesis: verum

end;

assume A3: for X being Subset of S st ex_sup_of X,L holds
"\/" X,L in S ; :: thesis: S is sups-closed

now

let X be Subset of (subrelstr S); :: thesis: ( ex_sup_of X,L implies "\/" X,L in the carrier of (subrelstr S) )
A4: X is Subset of S by YELLOW_0:def 15;
assume ex_sup_of X,L ; :: thesis: "\/" X,L in the carrier of (subrelstr S)
then "\/" X,L in S by A3, A4;
hence "\/" X,L in the carrier of (subrelstr S) by YELLOW_0:def 15; :: thesis: verum

end;

then subrelstr S is sups-inheriting by YELLOW_0:def 19;
hence S is sups-closed by Def4; :: thesis: verum