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 A1: ( ex_sup_of X,L & "\/" 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, YELLOW_0:65; :: thesis: verum