let X be set ; :: thesis: for f being PartFunc of X,ExtREAL
for A being set
for a being R_eal st A c= dom f holds
A /\ (less_dom f,a) = A \ (A /\ (great_eq_dom f,a))
let f be PartFunc of X,ExtREAL ; :: thesis: for A being set
for a being R_eal st A c= dom f holds
A /\ (less_dom f,a) = A \ (A /\ (great_eq_dom f,a))
let A be set ; :: thesis: for a being R_eal st A c= dom f holds
A /\ (less_dom f,a) = A \ (A /\ (great_eq_dom f,a))
let a be R_eal; :: thesis: ( A c= dom f implies A /\ (less_dom f,a) = A \ (A /\ (great_eq_dom f,a)) )
assume A1: A c= dom f ; :: thesis: A /\ (less_dom f,a) = A \ (A /\ (great_eq_dom f,a))
A2: dom f c= X by RELAT_1:def 18;
A3: A c= X by A1, A2, XBOOLE_1:1;
A4: for x being set st x in A /\ (less_dom f,a) holds
x in A \ (A /\ (great_eq_dom f,a))

proof

let x be set ; :: thesis: ( x in A /\ (less_dom f,a) implies x in A \ (A /\ (great_eq_dom f,a)) )
assume A5: x in A /\ (less_dom f,a) ; :: thesis: x in A \ (A /\ (great_eq_dom f,a))
A6: x in A by A5, XBOOLE_0:def 4;
A7: x in less_dom f,a by A5, XBOOLE_0:def 4;
A8: f . x < a by A7, Def12;
A9: not x in great_eq_dom f,a by A8, Def15;
A10: not x in A /\ (great_eq_dom f,a) by A9, XBOOLE_0:def 4;
thus x in A \ (A /\ (great_eq_dom f,a)) by A6, A10, XBOOLE_0:def 5; :: thesis: verum

end;

A11: A /\ (less_dom f,a) c= A \ (A /\ (great_eq_dom f,a)) by A4, TARSKI:def 3;
A12: for x being set st x in A \ (A /\ (great_eq_dom f,a)) holds
x in A /\ (less_dom f,a)

proof

let x be set ; :: thesis: ( x in A \ (A /\ (great_eq_dom f,a)) implies x in A /\ (less_dom f,a) )
assume A13: x in A \ (A /\ (great_eq_dom f,a)) ; :: thesis: x in A /\ (less_dom f,a)
A14: x in A by A13;
A15: not x in A /\ (great_eq_dom f,a) by A13, XBOOLE_0:def 5;
A16: not x in great_eq_dom f,a by A13, A15, XBOOLE_0:def 4;
reconsider x = x as Element of X by A3, A14;
reconsider y = f . x as R_eal ;
A17: not a <= y by A1, A14, A16, Def15;
A18: x in less_dom f,a by A1, A14, A17, Def12;
thus x in A /\ (less_dom f,a) by A13, A18, XBOOLE_0:def 4; :: thesis: verum

end;

A19: A \ (A /\ (great_eq_dom f,a)) c= A /\ (less_dom f,a) by A12, TARSKI:def 3;
thus A /\ (less_dom f,a) = A \ (A /\ (great_eq_dom f,a)) by A11, A19, XBOOLE_0:def 10; :: thesis: verum