let R be Relation; :: thesis: for X, Y being set st R quasi_orders Y & X c= Y holds
R quasi_orders X
let X, Y be set ; :: thesis: ( R quasi_orders Y & X c= Y implies R quasi_orders X )
assume that
A1: R is_reflexive_in Y and
A2: R is_transitive_in Y and
A3: X c= Y ; :: according to ORDERS_1:def 7 :: thesis: R quasi_orders X
thus ( R is_reflexive_in X & R is_transitive_in X ) by A1, A2, A3; :: according to ORDERS_1:def 7 :: thesis: verum