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