let E be set ; :: thesis: for A being Subset of E holds
( A ` c= A iff A = [#] E )
let A be Subset of E; :: thesis: ( A ` c= A iff A = [#] E )
thus ( A ` c= A implies A = [#] E ) :: thesis: ( A = [#] E implies A ` c= A )

proof

assume A ` c= A ; :: thesis: A = [#] E
hence A = A \/ (A ` ) by XBOOLE_1:12
.= [#] E by Th25 ;
:: thesis: verum

end;

assume A = [#] E ; :: thesis: A ` c= A
then A ` = {} by XBOOLE_1:37;
hence A ` c= A by XBOOLE_1:2; :: thesis: verum