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 ;
R is sups-inheriting ;
hence T is full infs-inheriting sups-inheriting SubRelStr of T by A1; :: thesis: verum