let C be non empty set ; :: thesis: for SC being Subset of C holds
( id SC is total iff SC = C )
let SC be Subset of C; :: thesis: ( id SC is total iff SC = C )
thus ( id SC is total implies SC = C ) :: thesis: ( SC = C implies id SC is total )

proof

assume id SC is total ; :: thesis: SC = C
then dom (id SC) = C by PARTFUN1:def 2;
hence SC = C by RELAT_1:45; :: thesis: verum

end;

assume SC = C ; :: thesis: id SC is total
then dom (id SC) = C by RELAT_1:45;
hence id SC is total by PARTFUN1:def 2; :: thesis: verum