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) )

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

thus ( B = eqSupport (f,X) implies B = (support f) /\ X ) :: thesis: ( B = (support f) /\ X implies B = eqSupport (f,X) )

proof

assume A3:
B = (support f) /\ X
; :: thesis: B = eqSupport (f,X)
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;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

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