defpred S_{1}[ 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_{1}[x,y] )

A8: for x being object st x in Class (PropRel Q) holds

S_{1}[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

$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

proof

consider F being Function of (Class (PropRel Q)),(Class (PropRel Q)) such that
let x be object ; :: thesis: ( x in Class (PropRel Q) implies ex y being object st

( y in Class (PropRel Q) & S_{1}[x,y] ) )

assume A2: x in Class (PropRel Q) ; :: thesis: ex y being object st

( y in Class (PropRel Q) & S_{1}[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_{1}[x,y] )

thus A4: y in Class (PropRel Q) by EQREL_1:def 3; :: thesis: S_{1}[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;( y in Class (PropRel Q) & S

assume A2: x in Class (PropRel Q) ; :: thesis: ex y being object st

( y in Class (PropRel Q) & S

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

thus A4: y in Class (PropRel Q) by EQREL_1:def 3; :: thesis: S

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

A8: for x being object st x in Class (PropRel Q) holds

S

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