let X, Y be set ; :: thesis: for P being Relation st P is_strongly_connected_in X & Y c= X holds
P is_strongly_connected_in Y
let P be Relation; :: thesis: ( P is_strongly_connected_in X & Y c= X implies P is_strongly_connected_in Y )
assume that
A1: P is_strongly_connected_in X and
A2: Y c= X ; :: thesis: P is_strongly_connected_in Y
let x be set ; :: according to RELAT_2:def 7 :: thesis: for b₁ being set holds
( not x in Y or not b₁ in Y or [x,b₁] in P or [b₁,x] in P )
let y be set ; :: thesis: ( not x in Y or not y in Y or [x,y] in P or [y,x] in P )
assume ( x in Y & y in Y ) ; :: thesis: ( [x,y] in P or [y,x] in P )
hence ( [x,y] in P or [y,x] in P ) by A1, A2, RELAT_2:def 7; :: thesis: verum