set R = first O;
thus first O is antisymmetric :: thesis: ( first O is transitive & first O is beta-transitive )

proof

let x be set ; :: according to MMLQUER2:def 2 :: thesis: for y being set st x,y in first O & y,x in first O holds
x = y
let y be set ; :: thesis: ( x,y in first O & y,x in first O implies x = y )
assume A1: ( x,y in first O & y,x in first O ) ; :: thesis: x = y
then reconsider x = x, y = y as Element of X by Th2;
y = y ;
then ( x . O <> {} & x . O = {} ) by A1, Def7;
hence x = y ; :: thesis: verum

end;

thus first O is transitive :: thesis: first O is beta-transitive

proof

let x be set ; :: according to MMLQUER2:def 1 :: thesis: for y, z being set st x,y in first O & y,z in first O holds
x,z in first O
let y, z be set ; :: thesis: ( x,y in first O & y,z in first O implies x,z in first O )
assume A2: ( x,y in first O & y,z in first O ) ; :: thesis: x,z in first O
then reconsider x = x, y = y, z = z as Element of X by Th2;
( x = x & z = z ) ;
then ( y . O <> {} & y . O = {} ) by A2, Def7;
hence x,z in first O ; :: thesis: verum

end;

let x, y be Element of X; :: according to MMLQUER2:def 4 :: thesis: ( x,y nin first O implies for z being Element of X st x,z in first O holds
y,z in first O )
assume A3: x,y nin first O ; :: thesis: for z being Element of X st x,z in first O holds
y,z in first O
let z be Element of X; :: thesis: ( x,z in first O implies y,z in first O )
assume x,z in first O ; :: thesis: y,z in first O
then A4: ( x . O <> {} & z . O = {} ) by Def7;
then y . O <> {} by A3, Def7;
hence y,z in first O by A4, Def7; :: thesis: verum