let L be non empty transitive RelStr ; :: thesis: for S being non empty full directed-sups-inheriting SubRelStr of L

for X being directed Subset of S st X <> {} & ex_sup_of X,L holds

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

let S be non empty full directed-sups-inheriting SubRelStr of L; :: thesis: for X being directed Subset of S st X <> {} & ex_sup_of X,L holds

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

let X be directed Subset of S; :: thesis: ( X <> {} & ex_sup_of X,L implies ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) )

assume that

A1: X <> {} and

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

"\/" (X,L) in the carrier of S by A1, A2, Def4;

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

for X being directed Subset of S st X <> {} & ex_sup_of X,L holds

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

let S be non empty full directed-sups-inheriting SubRelStr of L; :: thesis: for X being directed Subset of S st X <> {} & ex_sup_of X,L holds

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

let X be directed Subset of S; :: thesis: ( X <> {} & ex_sup_of X,L implies ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) )

assume that

A1: X <> {} and

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

"\/" (X,L) in the carrier of S by A1, A2, Def4;

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