defpred S₁[ object , object ] 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 object st x in Class (PropRel Q) holds
ex y being object st
( y in Class (PropRel Q) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Class (PropRel Q) implies ex y being object st
( y in Class (PropRel Q) & S₁[x,y] ) )
assume A2: x in Class (PropRel Q) ; :: thesis: ex y being object 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:36;
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 3; :: 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:20;
reconsider y9 = y as Subset of (Prop Q) ;
A7: 'not' q in y9 by EQREL_1:20;
p in x by A5, EQREL_1:20;
then 'not' p in y9 by A2, A4, A6, A7, Th11;
hence y = Class ((PropRel Q),('not' p)) by EQREL_1:23; :: thesis: verum

end;

consider F being Function of (Class (PropRel Q)),(Class (PropRel Q)) such that
A8: for x being object 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 3;
hence F . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) by A8; :: thesis: verum