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

set f = id L;

assume 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)) )

hence ex_sup_of (id L) .: X,L by FUNCT_1:92; :: thesis: "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L))

(id L) .: X = X by FUNCT_1:92;

hence "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) ; :: thesis: verum

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

set f = id L;

assume 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)) )

hence ex_sup_of (id L) .: X,L by FUNCT_1:92; :: thesis: "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L))

(id L) .: X = X by FUNCT_1:92;

hence "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) ; :: thesis: verum