let L be non empty transitive RelStr ; :: thesis: for C being non empty Subset of L

for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds

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

let C be non empty Subset of L; :: thesis: for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds

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

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

assume that

A1: ex_sup_of X,L and

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

the carrier of (subrelstr C) = C by YELLOW_0:def 15;

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

for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds

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

let C be non empty Subset of L; :: thesis: for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds

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

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

assume that

A1: ex_sup_of X,L and

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

the carrier of (subrelstr C) = C by YELLOW_0:def 15;

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