set N = {x} opp+id ;
A1: the carrier of ({x} opp+id ) = {x} by YELLOW_9:7;
thus {x} opp+id is transitive :: thesis: ( {x} opp+id is directed & {x} opp+id is monotone & {x} opp+id is antitone )

proof

let i, j, k be Element of ({x} opp+id ); :: according to YELLOW_0:def 2 :: thesis: ( not i <= j or not j <= k or i <= k )
( i = x & k = x ) by A1, TARSKI:def 1;
hence ( not i <= j or not j <= k or i <= k ) by YELLOW_0:def 1; :: thesis: verum

end;

thus {x} opp+id is directed :: thesis: ( {x} opp+id is monotone & {x} opp+id is antitone )

proof

let i, j be Element of ({x} opp+id ); :: according to YELLOW_6:def 5 :: thesis: ex b₁ being Element of the carrier of ({x} opp+id ) st
( i <= b₁ & j <= b₁ )
( i = x & j = x ) by A1, TARSKI:def 1;
then ( i <= i & j <= i ) ;
hence ex b₁ being Element of the carrier of ({x} opp+id ) st
( i <= b₁ & j <= b₁ ) ; :: thesis: verum

end;

thus {x} opp+id is monotone :: thesis: {x} opp+id is antitone

proof

let i, j be Element of ({x} opp+id ); :: according to WAYBEL_0:def 9,WAYBEL_1:def 2 :: thesis: ( not i <= j or (netmap ({x} opp+id ),T) . i <= (netmap ({x} opp+id ),T) . j )
( i = x & j = x ) by A1, TARSKI:def 1;
hence ( not i <= j or (netmap ({x} opp+id ),T) . i <= (netmap ({x} opp+id ),T) . j ) by YELLOW_0:def 1; :: thesis: verum

end;

let i, j be Element of ({x} opp+id ); :: according to WAYBEL21:def 2 :: thesis: ( i <= j implies ({x} opp+id ) . i >= ({x} opp+id ) . j )
( i = x & j = x ) by A1, TARSKI:def 1;
hence ( i <= j implies ({x} opp+id ) . i >= ({x} opp+id ) . j ) by YELLOW_0:def 1; :: thesis: verum