let L be non empty transitive RelStr ; :: thesis: for S being non empty sups-closed Subset of L

for X being Subset of S st ex_sup_of X,L holds

( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )

let S be non empty sups-closed Subset of L; :: thesis: for X being Subset of S st ex_sup_of X,L holds

( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )

let X be Subset of S; :: thesis: ( ex_sup_of X,L implies ( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) ) )

A1: X is Subset of (subrelstr S) by YELLOW_0:def 15;

assume A2: ex_sup_of X,L ; :: thesis: ( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )

subrelstr S is non empty full sups-inheriting SubRelStr of L by Def4;

then "\/" (X,L) in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def 19;

hence ( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) ) by A1, A2, YELLOW_0:64; :: thesis: verum

for X being Subset of S st ex_sup_of X,L holds

( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )

let S be non empty sups-closed Subset of L; :: thesis: for X being Subset of S st ex_sup_of X,L holds

( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )

let X be Subset of S; :: thesis: ( ex_sup_of X,L implies ( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) ) )

A1: X is Subset of (subrelstr S) by YELLOW_0:def 15;

assume A2: ex_sup_of X,L ; :: thesis: ( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )

subrelstr S is non empty full sups-inheriting SubRelStr of L by Def4;

then "\/" (X,L) in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def 19;

hence ( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) ) by A1, A2, YELLOW_0:64; :: thesis: verum