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