let X1, X2 be 1-sorted ; :: thesis: ( the carrier of X1 = the carrier of X2 implies for C1 being Subset of X1
for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` ) )
assume A1: the carrier of X1 = the carrier of X2 ; :: thesis: for C1 being Subset of X1
for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` )
let C1 be Subset of X1; :: thesis: for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` )
let C2 be Subset of X2; :: thesis: ( C1 = C2 iff C1 ` = C2 ` )
thus ( C1 = C2 implies C1 ` = C2 ` ) by A1; :: thesis: ( C1 ` = C2 ` implies C1 = C2 )
thus ( C1 ` = C2 ` implies C1 = C2 ) :: thesis: verum

proof

assume C1 ` = C2 ` ; :: thesis: C1 = C2
hence C1 = ([#] X2) \ (C2 `) by A1, PRE_TOPC:3
.= C2 by PRE_TOPC:3 ;
:: thesis: verum

end;