let L be non empty RelStr ; :: thesis: id L is directed-sups-preserving
let X be Subset of L; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or id L preserves_sup_of X )
assume ( not X is empty & X is directed ) ; :: thesis: id L preserves_sup_of X
assume A1: ex_sup_of X,L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (id L) .: X,L & "\/" ((id L) .: X),L = (id L) . ("\/" X,L) )
set f = id L;
A2: (id L) .: X = X by FUNCT_1:162;
thus ex_sup_of (id L) .: X,L by A1, FUNCT_1:162; :: thesis: "\/" ((id L) .: X),L = (id L) . ("\/" X,L)
thus "\/" ((id L) .: X),L = (id L) . ("\/" X,L) by A2, FUNCT_1:35; :: thesis: verum