let S be non empty RelStr ; :: thesis: for T being non empty reflexive antisymmetric RelStr
for t being Element of T
for X being non empty Subset of S holds
( S --> t preserves_sup_of X & S --> t preserves_inf_of X )
let T be non empty reflexive antisymmetric RelStr ; :: thesis: for t being Element of T
for X being non empty Subset of S holds
( S --> t preserves_sup_of X & S --> t preserves_inf_of X )
let t be Element of T; :: thesis: for X being non empty Subset of S holds
( S --> t preserves_sup_of X & S --> t preserves_inf_of X )
let X be non empty Subset of S; :: thesis: ( S --> t preserves_sup_of X & S --> t preserves_inf_of X )
set f = S --> t;
A1: S --> t = the carrier of S --> t by BORSUK_1:def 2;
A2: (S --> t) .: X = {t}

proof

thus (S --> t) .: X c= {t} by A1, BORSUK_1:6; :: according to XBOOLE_0:def 10 :: thesis: {t} c= (S --> t) .: X
consider x being Element of X;
( (S --> t) . x = t & the carrier of T <> {} ) by A1, FUNCOP_1:13;
then t in (S --> t) .: X by FUNCT_2:43;
hence {t} c= (S --> t) .: X by ZFMISC_1:37; :: thesis: verum

end;

( (S --> t) . (sup X) = t & (S --> t) . (inf X) = t & inf {t} = t & sup {t} = t & ex_sup_of {t},T & ex_inf_of {t},T ) by A1, FUNCOP_1:13, YELLOW_0:38, YELLOW_0:39;
hence ( S --> t preserves_sup_of X & S --> t preserves_inf_of X ) by A2, WAYBEL_0:def 30, WAYBEL_0:def 31; :: thesis: verum