let E be set ; :: thesis: ( E <> {} implies for B being Subset of E
for x being Element of E st not x in B holds
x in B ` )
assume A1: E <> {} ; :: thesis: for B being Subset of E
for x being Element of E st not x in B holds
x in B `
let B be Subset of E; :: thesis: for x being Element of E st not x in B holds
x in B `
let x be Element of E; :: thesis: ( not x in B implies x in B ` )
assume A2: not x in B ; :: thesis: x in B `
x in E by A1, Def1;
hence x in B ` by A2, XBOOLE_0:def 5; :: thesis: verum