let X be set ; :: thesis: for f being PartFunc of X,ExtREAL
for A being set
for a being ExtReal st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
let f be PartFunc of X,ExtREAL; :: thesis: for A being set
for a being ExtReal st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
let A be set ; :: thesis: for a being ExtReal st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
let a be ExtReal; :: thesis: ( A c= dom f implies A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) )
assume A1: A c= dom f ; :: thesis: A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
dom f c= X by RELAT_1:def 18;
then A2: A c= X by A1;
A3: A /\ (less_eq_dom (f,a)) c= A \ (A /\ (great_dom (f,a)))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A /\ (less_eq_dom (f,a)) or x in A \ (A /\ (great_dom (f,a))) )
assume A4: x in A /\ (less_eq_dom (f,a)) ; :: thesis: x in A \ (A /\ (great_dom (f,a)))
then A5: x in A by XBOOLE_0:def 4;
x in less_eq_dom (f,a) by A4, XBOOLE_0:def 4;
then f . x <= a by Def12;
then not x in great_dom (f,a) by Def13;
then not x in A /\ (great_dom (f,a)) by XBOOLE_0:def 4;
hence x in A \ (A /\ (great_dom (f,a))) by A5, XBOOLE_0:def 5; :: thesis: verum

end;

for x being object st x in A \ (A /\ (great_dom (f,a))) holds
x in A /\ (less_eq_dom (f,a))

proof

let x be object ; :: thesis: ( x in A \ (A /\ (great_dom (f,a))) implies x in A /\ (less_eq_dom (f,a)) )
assume A6: x in A \ (A /\ (great_dom (f,a))) ; :: thesis: x in A /\ (less_eq_dom (f,a))
then A7: x in A ;
not x in A /\ (great_dom (f,a)) by A6, XBOOLE_0:def 5;
then A8: not x in great_dom (f,a) by A6, XBOOLE_0:def 4;
reconsider x = x as Element of X by A2, A7;
reconsider y = f . x as R_eal ;
not a < y by A1, A7, A8, Def13;
then x in less_eq_dom (f,a) by A1, A7, Def12;
hence x in A /\ (less_eq_dom (f,a)) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

then A \ (A /\ (great_dom (f,a))) c= A /\ (less_eq_dom (f,a)) ;
hence A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) by A3, XBOOLE_0:def 10; :: thesis: verum