defpred S₁[ set , set ] means for p being Element of Prop Q st $1 = Class (PropRel Q),p holds
$2 = Class (PropRel Q),('not' p);
A1: for x being set st x in Class (PropRel Q) holds
ex y being set st
( y in Class (PropRel Q) & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in Class (PropRel Q) implies ex y being set st
( y in Class (PropRel Q) & S₁[x,y] ) )
assume A2: x in Class (PropRel Q) ; :: thesis: ex y being set st
( y in Class (PropRel Q) & S₁[x,y] )
then consider q being Element of Prop Q such that
A3: x = Class (PropRel Q),q by EQREL_1:45;
reconsider y = Class (PropRel Q),('not' q) as set ;
take y ; :: thesis: ( y in Class (PropRel Q) & S₁[x,y] )
thus A4: y in Class (PropRel Q) by EQREL_1:def 5; :: thesis: S₁[x,y]
let p be Element of Prop Q; :: thesis: ( x = Class (PropRel Q),p implies y = Class (PropRel Q),('not' p) )
assume A5: x = Class (PropRel Q),p ; :: thesis: y = Class (PropRel Q),('not' p)
then reconsider x = x as Subset of (Prop Q) ;
A6: q in x by A3, EQREL_1:28;
reconsider y9 = y as Subset of (Prop Q) ;
A7: 'not' q in y9 by EQREL_1:28;
p in x by A5, EQREL_1:28;
then 'not' p in y9 by A2, A4, A6, A7, Th33;
hence y = Class (PropRel Q),('not' p) by EQREL_1:31; :: thesis: verum

end;

consider F being Function of (Class (PropRel Q)),(Class (PropRel Q)) such that
A8: for x being set st x in Class (PropRel Q) holds
S₁[x,F . x] from FUNCT_2:sch 1(A1);
take F ; :: thesis: for p being Element of Prop Q holds F . (Class (PropRel Q),p) = Class (PropRel Q),('not' p)
let p be Element of Prop Q; :: thesis: F . (Class (PropRel Q),p) = Class (PropRel Q),('not' p)
Class (PropRel Q),p in Class (PropRel Q) by EQREL_1:def 5;
hence F . (Class (PropRel Q),p) = Class (PropRel Q),('not' p) by A8; :: thesis: verum