let Q be Quantum_Mechanics; :: thesis: for B, C being Subset of (Prop Q) st B in Class (PropRel Q) & C in Class (PropRel Q) holds
for p, q being Element of Prop Q st 'not' p in C & 'not' q in C & p in B holds
q in B
let B, C be Subset of (Prop Q); :: thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) implies for p, q being Element of Prop Q st 'not' p in C & 'not' q in C & p in B holds
q in B )
assume A1: ( B in Class (PropRel Q) & C in Class (PropRel Q) ) ; :: thesis: for p, q being Element of Prop Q st 'not' p in C & 'not' q in C & p in B holds
q in B
let p, q be Element of Prop Q; :: thesis: ( 'not' p in C & 'not' q in C & p in B implies q in B )
( 'not' ('not' p) = p & 'not' ('not' q) = q ) ;
hence ( 'not' p in C & 'not' q in C & p in B implies q in B ) by A1, Th11; :: thesis: verum