let X1 be non empty set ; :: thesis: for A1 being Subset of X1 holds A1 ` = { x1 where x1 is Element of X1 : not x1 in A1 }
let A1 be Subset of X1; :: thesis: A1 ` = { x1 where x1 is Element of X1 : not x1 in A1 }
thus A1 ` c= { x1 where x1 is Element of X1 : not x1 in A1 } :: according to XBOOLE_0:def 10 :: thesis: { x1 where x1 is Element of X1 : not x1 in A1 } c= A1 `
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A1 ` or a in { x1 where x1 is Element of X1 : not x1 in A1 } )
assume A1: a in A1 ` ; :: thesis: a in { x1 where x1 is Element of X1 : not x1 in A1 }
then not a in A1 by XBOOLE_0:def 5;
hence a in { x1 where x1 is Element of X1 : not x1 in A1 } by A1; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x1 where x1 is Element of X1 : not x1 in A1 } or a in A1 ` )
assume a in { x1 where x1 is Element of X1 : not x1 in A1 } ; :: thesis: a in A1 `
then ex x1 being Element of X1 st
( a = x1 & not x1 in A1 ) ;
hence a in A1 ` by SUBSET_1:29; :: thesis: verum