let N be non empty RelStr ; :: thesis: ( N is directed iff RelStr(# the carrier of N, the InternalRel of N #) is directed )
thus ( N is directed implies RelStr(# the carrier of N, the InternalRel of N #) is directed ) :: thesis: ( RelStr(# the carrier of N, the InternalRel of N #) is directed implies N is directed )
proof
assume A1: N is directed ; :: thesis: RelStr(# the carrier of N, the InternalRel of N #) is directed
let x, y be Element of RelStr(# the carrier of N, the InternalRel of N #); :: according to YELLOW_6:def 3 :: thesis: ex z being Element of RelStr(# the carrier of N, the InternalRel of N #) st
( x <= z & y <= z )
reconsider x9 = x, y9 = y as Element of N ;
consider z9 being Element of N such that
A2: ( x9 <= z9 & y9 <= z9 ) by A1;
reconsider z = z9 as Element of RelStr(# the carrier of N, the InternalRel of N #) ;
take z ; :: thesis: ( x <= z & y <= z )
( [x,z] in the InternalRel of N & [y,z] in the InternalRel of N ) by A2, ORDERS_2:def 5;
hence ( x <= z & y <= z ) by ORDERS_2:def 5; :: thesis: verum
end;
assume A3: RelStr(# the carrier of N, the InternalRel of N #) is directed ; :: thesis: N is directed
let x, y be Element of N; :: according to YELLOW_6:def 3 :: thesis: ex z being Element of N st
( x <= z & y <= z )
reconsider x9 = x, y9 = y as Element of RelStr(# the carrier of N, the InternalRel of N #) ;
consider z9 being Element of RelStr(# the carrier of N, the InternalRel of N #) such that
A4: ( x9 <= z9 & y9 <= z9 ) by A3;
reconsider z = z9 as Element of N ;
take z ; :: thesis: ( x <= z & y <= z )
( [x9,z9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) & [y9,z9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) ) by A4, ORDERS_2:def 5;
hence ( x <= z & y <= z ) by ORDERS_2:def 5; :: thesis: verum