let A be non empty set ; :: thesis: for B, C being non empty Subset of A

for D being non empty Subset of B st C = D holds

incl C = (incl B) * (incl D)

let B, C be non empty Subset of A; :: thesis: for D being non empty Subset of B st C = D holds

incl C = (incl B) * (incl D)

let D be non empty Subset of B; :: thesis: ( C = D implies incl C = (incl B) * (incl D) )

assume A1: C = D ; :: thesis: incl C = (incl B) * (incl D)

(incl B) * (incl D) = id (B /\ D) by FUNCT_1:22

.= incl C by A1, XBOOLE_1:28 ;

hence incl C = (incl B) * (incl D) ; :: thesis: verum

for D being non empty Subset of B st C = D holds

incl C = (incl B) * (incl D)

let B, C be non empty Subset of A; :: thesis: for D being non empty Subset of B st C = D holds

incl C = (incl B) * (incl D)

let D be non empty Subset of B; :: thesis: ( C = D implies incl C = (incl B) * (incl D) )

assume A1: C = D ; :: thesis: incl C = (incl B) * (incl D)

(incl B) * (incl D) = id (B /\ D) by FUNCT_1:22

.= incl C by A1, XBOOLE_1:28 ;

hence incl C = (incl B) * (incl D) ; :: thesis: verum