let Y1, Y2 be Subset of [:S, the carrier of A:]; :: thesis: ( [:S,(ElementaryInstructions A):] c= Y1 & [:S,{(EmptyIns A)}:] c= Y1 & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in Y1 & [(f . (s,I)),J] in Y1 implies [s,(I \; J)] in Y1 ) & ( [s,C] in Y1 & [(f . (s,C)),I] in Y1 & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in Y1 ) & ( [s,C] in Y1 & [(f . (s,C)),J] in Y1 & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in Y1 ) & ( [s,C] in Y1 & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in Y1 & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in Y1 ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
Y1 c= P ) & [:S,(ElementaryInstructions A):] c= Y2 & [:S,{(EmptyIns A)}:] c= Y2 & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in Y2 & [(f . (s,I)),J] in Y2 implies [s,(I \; J)] in Y2 ) & ( [s,C] in Y2 & [(f . (s,C)),I] in Y2 & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in Y2 ) & ( [s,C] in Y2 & [(f . (s,C)),J] in Y2 & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in Y2 ) & ( [s,C] in Y2 & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in Y2 & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in Y2 ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
Y2 c= P ) implies Y1 = Y2 )
assume that
A28: S₁[Y1] and
A29: for Y being Subset of [:S, the carrier of A:] st S₁[Y] holds
Y1 c= Y and
A30: S₁[Y2] and
A31: for Y being Subset of [:S, the carrier of A:] st S₁[Y] holds
Y2 c= Y ; :: thesis: Y1 = Y2
thus Y1 c= Y2 by A29, A30; :: according to XBOOLE_0:def 10 :: thesis: Y2 c= Y1
thus Y2 c= Y1 by A28, A31; :: thesis: verum