let T be non empty RelStr ; :: thesis: T is full infs-inheriting sups-inheriting SubRelStr of T
reconsider R = T as full SubRelStr of T by YELLOW_6:6;
A1: R is infs-inheriting

proof

let X be Subset of R; :: according to YELLOW_0:def 18 :: thesis: ( not ex_inf_of X,T or "/\" (X,T) in the carrier of R )
thus ( not ex_inf_of X,T or "/\" (X,T) in the carrier of R ) ; :: thesis: verum

end;

R is sups-inheriting

proof

let X be Subset of R; :: according to YELLOW_0:def 19 :: thesis: ( not ex_sup_of X,T or "\/" (X,T) in the carrier of R )
thus ( not ex_sup_of X,T or "\/" (X,T) in the carrier of R ) ; :: thesis: verum

end;

hence T is full infs-inheriting sups-inheriting SubRelStr of T by A1; :: thesis: verum