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 by A1, TARSKI:def 1;
hence ( not i <= j or not j <= k or i <= k ) by A1, TARSKI: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₁ )
A2: i = x by A1, TARSKI:def 1;
A3: i <= i ;
j <= i by A1, A2, TARSKI:def 1;
hence ex b₁ being Element of the carrier of ({x} opp+id ) st
( i <= b₁ & j <= b₁ ) by A3; :: 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 )
A4: i = x by A1, TARSKI:def 1;
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 A4, 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 )
A5: i = x by A1, TARSKI:def 1;
j = x by A1, TARSKI:def 1;
hence ( i <= j implies ({x} opp+id ) . i >= ({x} opp+id ) . j ) by A5, YELLOW_0:def 1; :: thesis: verum