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 Th10 ;
:: thesis: verum
end;
thus ( A = [#] E implies A ` c= A ) by XBOOLE_1:37; :: thesis: verum