let S be non empty SubRelStr of A; :: thesis: ( S is full implies S is connected )

assume A1: S is full ; :: thesis: S is connected

for x, y being Element of S holds

( x <= y or y <= x )

assume A1: S is full ; :: thesis: S is connected

for x, y being Element of S holds

( x <= y or y <= x )

proof

hence
S is connected
by WAYBEL_0:def 29; :: thesis: verum
let x, y be Element of S; :: thesis: ( x <= y or y <= x )

A2: the carrier of S c= the carrier of A by YELLOW_0:def 13;

reconsider b = y as Element of A by A2;

reconsider a = x as Element of A by A2;

( a <= b or b <= a ) by WAYBEL_0:def 29;

hence ( x <= y or y <= x ) by A1, YELLOW_0:60; :: thesis: verum

end;A2: the carrier of S c= the carrier of A by YELLOW_0:def 13;

reconsider b = y as Element of A by A2;

reconsider a = x as Element of A by A2;

( a <= b or b <= a ) by WAYBEL_0:def 29;

hence ( x <= y or y <= x ) by A1, YELLOW_0:60; :: thesis: verum