let x be Element of X; :: thesis: (x `) ` = x `
x \ (x `) = (x \ (0. X)) \ (x `) by Th2;
then x \ (x `) in { x2 where x2 is Element of X : 0. X <= x2 } by A1;
then ex x2 being Element of X st
( x \ (x `) = x2 & 0. X <= x2 ) ;
then (x \ (x `)) ` = 0. X ;
then A2: (x `) \ ((x `) `) = 0. X by Th9;
(x `) \ x = (x `) \ (x \ (0. X)) by Th2;
then (x `) \ x in { x1 where x1 is Element of X : 0. X <= x1 } by A1;
then ex x1 being Element of X st
( (x `) \ x = x1 & 0. X <= x1 ) ;
then ((x `) \ x) ` = 0. X ;
then ((x `) `) \ (x `) = 0. X by Th9;
hence (x `) ` = x ` by A2, Def7; :: thesis: verum