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 ;
let X be Subset of S; :: thesis: ( ex_sup_of X,L implies "\/" (X,L) in S )
assume A2: ex_sup_of X,L ; :: thesis: "\/" (X,L) in S
X is Subset of () by YELLOW_0:def 15;
then "\/" (X,L) in the carrier of () by A1, A2;
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 :: thesis: for X being Subset of () st ex_sup_of X,L holds
"\/" (X,L) in the carrier of ()
let X be Subset of (); :: thesis: ( ex_sup_of X,L implies "\/" (X,L) in the carrier of () )
assume A4: ex_sup_of X,L ; :: thesis: "\/" (X,L) in the carrier of ()
X is Subset of S by YELLOW_0:def 15;
then "\/" (X,L) in S by A3, A4;
hence "\/" (X,L) in the carrier of () by YELLOW_0:def 15; :: thesis: verum
end;
then subrelstr S is sups-inheriting ;
hence S is sups-closed ; :: thesis: verum