let S be SubRelStr of L; :: thesis: ( S is sups-inheriting implies S is join-inheriting )
assume A2: for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in the carrier of S ; :: according to YELLOW_0:def 19 :: thesis: S is join-inheriting
let x, y be Element of L; :: according to YELLOW_0:def 17 :: thesis: ( x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L implies sup {x,y} in the carrier of S )
assume ( x in the carrier of S & y in the carrier of S ) ; :: thesis: ( not ex_sup_of {x,y},L or sup {x,y} in the carrier of S )
then {x,y} c= the carrier of S by ZFMISC_1:32;
hence ( not ex_sup_of {x,y},L or sup {x,y} in the carrier of S ) by A2; :: thesis: verum