let B be Subset of A; :: thesis: ( B = eqSupport (f,X) iff B = (support f) /\ X )
thus ( B = eqSupport (f,X) implies B = (support f) /\ X ) :: thesis: ( B = (support f) /\ X implies B = eqSupport (f,X) )
proof
assume B = eqSupport (f,X) ; :: thesis: B = (support f) /\ X
then consider D being a_partition of the carrier of A, Y being Element of D such that
D = the carrier of (QuotientOrder A) and
A1: Y = X and
A2: B = eqSupport (f,Y) by Def12;
thus B = (support f) /\ X by A1, A2; :: thesis: verum
end;
assume A3: B = (support f) /\ X ; :: thesis: B = eqSupport (f,X)
reconsider D = the carrier of (QuotientOrder A) as a_partition of the carrier of A by Th47;
reconsider Y = X as Element of D ;
thus B = eqSupport (f,Y) by A3
.= eqSupport (f,X) by Def12 ; :: thesis: verum