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) .: X = {t}

proof

thus (S --> t) .: X c= {t} by FUNCOP_1:81; :: according to XBOOLE_0:def 10 :: thesis: {t} c= (S --> t) .: X
set x = the Element of X;
(S --> t) . the Element of X = t by FUNCOP_1:7;
then t in (S --> t) .: X by FUNCT_2:35;
hence {t} c= (S --> t) .: X by ZFMISC_1:31; :: thesis: verum

end;

A2: (S --> t) . (sup X) = t by FUNCOP_1:7;
A3: (S --> t) . (inf X) = t by FUNCOP_1:7;
A4: inf {t} = t by YELLOW_0:39;
A5: sup {t} = t by YELLOW_0:39;
A6: ex_sup_of {t},T by YELLOW_0:38;
ex_inf_of {t},T by YELLOW_0:38;
hence ( S --> t preserves_sup_of X & S --> t preserves_inf_of X ) by A1, A2, A3, A4, A5, A6; :: thesis: verum