let X be non empty set ; :: thesis: for R, S, T being Membership_Func of X st S c= & T c= holds

T c=

let R, S, T be Membership_Func of X; :: thesis: ( S c= & T c= implies T c= )

assume A1: ( S c= & T c= ) ; :: thesis: T c=

for x being Element of X holds R . x <= T . x

T c=

let R, S, T be Membership_Func of X; :: thesis: ( S c= & T c= implies T c= )

assume A1: ( S c= & T c= ) ; :: thesis: T c=

for x being Element of X holds R . x <= T . x

proof

hence
T c=
; :: thesis: verum
let x be Element of X; :: thesis: R . x <= T . x

( R . x <= S . x & S . x <= T . x ) by A1;

hence R . x <= T . x by XXREAL_0:2; :: thesis: verum

end;( R . x <= S . x & S . x <= T . x ) by A1;

hence R . x <= T . x by XXREAL_0:2; :: thesis: verum