set R = first O;
thus
first O is antisymmetric
( first O is transitive & first O is beta-transitive )
thus
first O is transitive
first O is beta-transitive proof
let x be
set ;
MMLQUER2:def 1 for y, z being set st x,y in first O & y,z in first O holds
x,z in first Olet y,
z be
set ;
( 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 )
;
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
;
verum
end;
let x, y be Element of X; MMLQUER2:def 4 ( 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
; for z being Element of X st x,z in first O holds
y,z in first O
let z be Element of X; ( x,z in first O implies y,z in first O )
assume
x,z in first O
; 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; verum